[isabelle] Where I could find the Schroeder-Bernstein The... · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Where I could find the Schroeder-Bernstein The...

Email Gateway (Aug 22 2022 at 18:29):

From: Tobias Nipkow <nipkow@in.tum.de>
It is part of Main:

thm Schroeder_Bernstein

There are two proofs. You can find both versions by grepping for Schroeder.

Tobias
smime.p7s

Email Gateway (Aug 22 2022 at 18:29):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
... and a version for arbitrary sets:

theory Draft

imports "HOL-Library.Cardinal_Notations"

begin

lemma "inj_on f A ⟹ inj_on g B ⟹ f A ⊆ B ⟹ g B ⊆ A ⟹ |A| =o |B|"

by (meson Schroeder_Bernstein card_of_ordIso)

end

Best wishes,

Andrei

From: cl-isabelle-users-bounces@lists.cam.ac.uk <cl-isabelle-users-bounces@lists.cam.ac.uk> on behalf of Tobias Nipkow <nipkow@in.tum.de>
Sent: 12 September 2018 14:34:08
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Where I could find the Schroeder-Bernstein Theorem?

It is part of Main:

thm Schroeder_Bernstein

There are two proofs. You can find both versions by grepping for Schroeder.

Tobias

On 12/09/2018 13:19, José Manuel Rodriguez Caballero wrote:

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
The Top 100 Theorems in Isabelle - Computer Science and ...<http://www.cse.unsw.edu.au/~kleing/top100/>
www.cse.unsw.edu.au
The following are the theorems from this list proved so far in the Isabelle proof assistant. If you have proved additional ones or know of any, please send me email so I can add them here. If the theorem is not part of the Isabelle distribution, the entry will usually contain a link to the ...

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

Email Gateway (Aug 22 2022 at 18:30):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Sorry for my confusing previous message. General cardinals are of course not needed, as the theorem is available from a pre-cardinal theory.

Best wishes,

Andrei

From: Andrei Popescu
Sent: 12 September 2018 15:04:21
To: cl-isabelle-users@lists.cam.ac.uk
Subject: Re: [isabelle] Where I could find the Schroeder-Bernstein Theorem?

... and a version for arbitrary sets:

theory Draft
imports "HOL-Library.Cardinal_Notations"
begin

lemma "inj_on f A ⟹ inj_on g B ⟹ f A ⊆ B ⟹ g B ⊆ A ⟹ |A| =o |B|"
by (meson Schroeder_Bernstein card_of_ordIso)

end

Best wishes,

Andrei

It is part of Main:

thm Schroeder_Bernstein

There are two proofs. You can find both versions by grepping for Schroeder.

Tobias

On 12/09/2018 13:19, José Manuel Rodriguez Caballero wrote:

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
The Top 100 Theorems in Isabelle - Computer Science and ...<http://www.cse.unsw.edu.au/~kleing/top100/>
www.cse.unsw.edu.au
The following are the theorems from this list proved so far in the Isabelle proof assistant. If you have proved additional ones or know of any, please send me email so I can add them here. If the theorem is not part of the Isabelle distribution, the entry will usually contain a link to the ...

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

Email Gateway (Aug 22 2022 at 18:30):

From: Makarius <makarius@sketis.net>
BTW, in Oct-2016 I have reworked your proof and one of my former
HOL-Isar_Examples, to make the version of theorem Schroeder_Bernstein
that is presently in Main HOL (and thus easy to find via "find_theorems
name: Bernstein").

That version does not require Hilbert-Choice (or other versions of
Choice): it uses "the_inv" instead of the more common "inv" operator. It
also cannot use the proof method "metis", which uses Hilbert-Choice
internally, so the final "by (metis ComplI)" has become a bit more
cumbersome.

Nonetheless, I've tried hard to produce a good Isar proof: that example
emerged from some course on Isabelle some years ago.

Makarius

Email Gateway (Aug 22 2022 at 18:30):

From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Makarius,

Indeed, very nice that the theorem now only depends on definite choice.

Best wishes,

Andrei

BTW, in Oct-2016 I have reworked your proof and one of my former
HOL-Isar_Examples, to make the version of theorem Schroeder_Bernstein
that is presently in Main HOL (and thus easy to find via "find_theorems
name: Bernstein").

Nonetheless, I've tried hard to produce a good Isar proof: that example
emerged from some course on Isabelle some years ago.

Makarius

Last updated: Apr 19 2024 at 12:27 UTC