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 file set_theory.cardinal.

source

theorem function.embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : function.injective f) (hg : function.injective g) :

∃ (h : α → β), function.bijective h

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

source

theorem function.embedding.antisymm {α : Type u} {β : Type v} :

(α ↪ β) → (β ↪ α) → nonempty (α ≃ β)

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

source

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.linear_order for (one of) the lattice instance.

source

theorem function.embedding.total {α : Type u} {β : Type v} :

nonempty (α ↪ β) ∨ nonempty (β ↪ α)

The cardinals are totally ordered. See cardinal.linear_order for (one of) the lattice instance.