Schröder-Bernstein theorem, well-ordering of cardinals #
Cardinals are naturally ordered by
α ≤ β ↔ ∃ f : a → β, 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 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.