Schröder-Bernstein theorem, well-ordering of cardinals

This file proves the Schröder-Bernstein theorem (see schroeder_bernstein), the well-ordering of cardinals (see min_injective) and the totality of their order (see total).

Notes

Cardinals are naturally ordered by α ≤ β ↔ ∃ f : a → β, Injective f:

• schroeder_bernstein states that, given injections α → β and β → α, one can get a bijection α → β. This corresponds to the antisymmetry of the order.
• The order is also well-founded: any nonempty set of cardinals has a minimal element. min_injective states that by saying that there exists an element of the set that injects into all others.

Cardinals are defined and further developed in the folder SetTheory.Cardinal.

theorem Function.Embedding.schroeder_bernstein_of_rel {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) (R : α → β → Prop) (hp₁ : ∀ (a : α), R a (f a)) (hp₂ : ∀ (b : β), R (g b) b) : ∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)

The Schröder-Bernstein Theorem: Given injections α → β and β → α that satisfy a pointwise property R, we can get a bijection α → β that satisfies that same pointwise property.

theorem Function.Embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) : ∃ (h : α → β), Bijective h

The Schröder-Bernstein Theorem: Given injections α → β and β → α, we can get a bijection α → β.

theorem Function.Embedding.antisymm {α : Type u} {β : Type v} : ∀ (a : α ↪ β) (a✝ : β ↪ α), Nonempty (α ≃ β)

The Schröder-Bernstein Theorem: Given embeddings α ↪ β and β ↪ α, there exists an equivalence α ≃ β.

theorem Function.Embedding.min_injective {ι : Type u} (β : ι → Type v) [I : Nonempty ι] : ∃ (i : ι), Nonempty ((j : ι) → β i ↪ β j)

The cardinals are well-ordered. We express it here by the fact that in any set of cardinals there is an element that injects into the others. See Cardinal.conditionallyCompleteLinearOrderBot for (one of) the lattice instances.

theorem Function.Embedding.total (α : Type u) (β : Type v) : Nonempty (α ↪ β) ∨ Nonempty (β ↪ α)

The cardinals are totally ordered. See Cardinal.conditionallyCompleteLinearOrderBot for (one of) the lattice instance.