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

.

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 `α → β`

.

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.