# 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`

:

`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 folder `SetTheory.Cardinal`

.

**The Schröder-Bernstein Theorem**:
Given injections `α → β→ β`

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.conditionallyCompleteLinearOrderBot`

for (one of) the lattice instances.