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.


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

how can i write and prove:

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


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