Email Gateway (Aug 18 2022 at 16:45): Email Gateway (Aug 18 2022 at 16:45):From: Victor Porton <porton@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(?gy) =
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
Email Gateway (Aug 18 2022 at 16:45):From: Victor Porton <porton@narod.ru>
18.12.2010, 23:29, "Victor Porton" <porton@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(?gy)
= 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(gy) =
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
Last updated: Apr 26 2024 at 16:20 UTC