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

source
theorem Function.Embedding.schroeder_bernstein_of_rel {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) (R : α → β → Prop) (hp₁ : ∀ (a : α), R a (f a)) (hp₂ : ∀ (b : β), R (g b) b) :
∃ (h : α → β), Bijective h ∧ ∀ (a : α), R a (h a)

The Schröder-Bernstein Theorem: Given injections `α → β` and `β → α` that satisfy a pointwise property `R`, we can get a bijection `α → β` that satisfies that same pointwise property.

source
theorem Function.Embedding.schroeder_bernstein {α : Type u} {β : Type v} {f : α → β} {g : β → α} (hf : Injective f) (hg : Injective g) :
∃ (h : α → β), Bijective h

The Schröder-Bernstein Theorem: Given injections `α → β` and `β → α`, we can get a bijection `α → β`.

source
theorem Function.Embedding.antisymm {α : Type u} {β : Type v} :
∀ (a : α ↪ β) (a✝ : β ↪ α), Nonempty (α ≃ β)

The Schröder-Bernstein Theorem: Given embeddings `α ↪ β` and `β ↪ α`, there exists an equivalence `α ≃ β`.

source
theorem Function.Embedding.min_injective {ι : Type u} (β : ι → Type v) [I : Nonempty ι] :
∃ (i : ι), Nonempty ((j : ι) → β i ↪ β j)

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.

source
theorem Function.Embedding.total (α : Type u) (β : Type v) :
Nonempty (α ↪ β) ∨ Nonempty (β ↪ α)

The cardinals are totally ordered. See `Cardinal.conditionallyCompleteLinearOrderBot` for (one of) the lattice instance.