[isabelle] Should add new lemma to ZF core?
I suggest to add the following lemma similar to existing comp_eq_id_iff lemma to ZF core.
"[| f: Af->B; g: B->Ag; Ag<=Af |] ==> f O g = id(B) <-> (ALL y:B. f`(?g`y) = y)"
I am thinking about how to prove it, but have not yet proved.
Proofs are welcomed.
So: Will we add it to ZF core or not? (Please say your options and imperatives.)
Victor Porton - http://portonvictor.org
This archive was generated by a fusion of
Pipermail (Mailman edition) and