Cantor_Bernstein

Stream: Is there code for X?

[Chris Birkbeck]

Is the following result somewhere in mathlib?

noncomputable def Cantor_Bernstein {α : Type u} {β : Type u} (f: α → β) (g : β → α )
    (h1 : function.injective f) (h2 :function.injective g) : α ≃ β :=
begin
have c1 := cardinal.mk_le_of_injective h1,
have c2 :=cardinal.mk_le_of_injective h2,
have c3 : cardinal.mk α =cardinal.mk β , by {exact le_antisymm c1 c2,  },
apply (cardinal.eq.1 c3).some,
end

It feels like it should, but I couldn't find it. If not, any ideas where to put it?

[Adam Topaz]

I'm inclined to say that it should go somewhere around set_theory.cardinal. Also, it would be better to not require $\alpha$ and $\beta$ to be in the same universe.

[Johan Commelin]

I would be surprised if this isn't there yet

[Anne Baanen]

docs#function.embedding.schroeder_bernstein

[Anne Baanen]

I know this result as Cantor-Schröder-Bernstein, so I searched for each of the names in turn until I found it :D

[Chris Birkbeck]

ahh wonderful! I knew it had to be somewhere

[Adam Topaz]

Anne Baanen said:

docs#function.embedding.schroeder_bernstein

The proof of this is 25 lines long!

[Kevin Buzzard]

Yes but does it assume le_antisymm for cardinals?

[Anne Baanen]

set_theory/cardinal.lean depends on the theorem, so probably not

[Kevin Buzzard]

Right!

[Adam Topaz]

Ah :)

[Kevin Buzzard]

So in fact your proof is probably circular Chris :-)

[Chris Birkbeck]

Kevin Buzzard said:

So in fact your proof is probably circular Chris :-)

Ah yes the best kind of proof!

[Riccardo Brasca]

le_antisymm is proved by le_antisymm := by { rintros ⟨α⟩ ⟨β⟩ ⟨e₁⟩ ⟨e₂⟩, exact quotient.sound (e₁.antisymm e₂) }, and antisymm is

theorem antisymm : (α ↪ β) → (β ↪ α) → nonempty (α ≃ β)
| ⟨e₁, h₁⟩ ⟨e₂, h₂⟩ :=
  let ⟨f, hf⟩ := schroeder_bernstein h₁ h₂ in
  ⟨equiv.of_bijective f hf⟩

So it's indeed circular :)

[Riccardo Brasca]

BTW, a good method to find it is to look for the linear_order instance on cardidal, that is found automatically by Lean, and see how antisymmetry is proved.

[Riccardo Brasca]

I always use Kevin's trick described here to explicitly find the instance. No idea if there are better ways of doing it.