Re: [isabelle] Quantifier over empty set



Hi Roger,

If the symbol ∅ denotes the empty map Map.empty, then you cannot. dom ∅ = {}, so you quantify over an empty set, and this is always True, even if B is False.

Andreas

On 07/01/14 11:26, Roger H. wrote:
Hi,

how can i write and prove:

"A = ∅ ⟹ (∀c∈dom A. B) = B"

Thanks
  		 	   		





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.