Schröder-Bernstein theorem, well-ordering of cardinals #
This file proves the Schröder-Bernstein theorem (see
schroeder_bernstein), the well-ordering of
min_injective) and the totality of their order (see
Cardinals are naturally ordered by
α ≤ β ↔ ∃ f : a → β, Injective f≤ β ↔ ∃ f : a → β, Injective f↔ ∃ f : a → β, Injective f∃ f : a → β, Injective f→ β, Injective f:
schroeder_bernsteinstates 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_injectivestates 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
The Schröder-Bernstein Theorem:
α → β→ β and
β → α→ α, we can get a bijection
α → β→ β.
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.
Cardinal.conditionallyCompleteLinearOrderBot for (one of) the lattice instances.