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≤ β ↔ ∃ f : a → β, Injective f↔ ∃ f : a → β, Injective f∃ f : a → β, Injective f→ β, Injective f:

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

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

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

theorem Function.Embedding.antisymm {α : Type u} {β : Type v} :
(α β) → (β α) → 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 (α : Type u) (β : Type v) :
Nonempty (α β) Nonempty (β α)

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