Email Gateway (Aug 22 2022 at 18:29): Email Gateway (Aug 22 2022 at 18:29):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
I was implementing a number-theoretic proof where I used the following
finite version of Schroeder-Bernstein Theorem:
definition injfun:: ‹('a ⇒ 'b) ⇒ 'a set ⇒ bool› where
‹injfun ≡ λ f. λ A. (∀ x y::'a. x ∈ A ∧ y ∈ A ∧ f x = f y ⟶ x = y )›
definition typefun:: ‹('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ bool› where
‹typefun ≡ λ f. λ A. λ B. (∀ x ::'a. (x ∈ A ⟶ f x ∈ B) )›
lemma CantorBernsteinSchroeder:
fixes A :: ‹'a set› and B :: ‹'b set› and f :: ‹'a ⇒ 'b› and g :: ‹'b ⇒
'a›
assumes ‹typefun f A B› and ‹typefun g B A› and ‹injfun f A› and ‹injfun
g B›
and ‹finite A› and ‹finite B›
shows ‹card A = card B›
Although I can prove this auxiliary result by myself, this was already done
in Isabelle/HOL. Indeed in the Top 100 Theorems in Isabelle (
http://www.cse.unsw.edu.au/~kleing/top100/) a more general version of this
result is in position 25:
lemma schroeder_bernstein:
"[| f ∈ inj(X,Y); g ∈ inj(Y,X) |] ==> ∃h. h ∈ bij(X,Y)"
So, my question is: Where I could find this theorem in order to obtain the
particular version that I need as a trivial consequence? Thank you in
advance.
Kind Regards,
José M.
https://github.com/josephcmac/Folklore-and-miscellaneous-results-in-number-theory
Last updated: Nov 21 2024 at 12:39 UTC