Schröder-Bernstein theorem, well-ordering of cardinals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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:
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 file
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. See
cardinal.linear_order for (one of) the