Re: [isabelle] Should add new lemma to ZF core?



18.12.2010, 23:29, "Victor Porton" <porton at narod.ru>:
I suggest to add the following lemma similar to existing comp_eq_id_iff lemma to ZF core.
 
lemma comp_eq_id_iff2:
  "[| 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.)
 
Above I wrote a superfluous question sign. "?g" should be replaced with "g".
 
Oh, well, it seems that it also can be generalized (replacing Af->B with Af->C):
 
lemma comp_eq_id_iff2:
  "[| f: Af->C; g: B->Ag; Ag<=Af |] ==> f O g = id(B) <-> (ALL y:B. f`(g`y) = y)"
 
So will we add the last version of the above lemma to Isabelle/ZF or will we not? Some answer to this question is necessary.
 
--
Victor Porton - http://portonvictor.org


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