Function.Embedding.total
theorem Function.Embedding.total : ∀ (α : Type u) (β : Type v), Nonempty (α ↪ β) ∨ Nonempty (β ↪ α)
This theorem states that for any two types `α` and `β`, there exists a total order between their cardinalities. Specifically, either there is a nonempty embedding from `α` to `β`, or there is a nonempty embedding from `β` to `α`. An embedding here refers to an injective (one-to-one) function from one type to another. Thus, the cardinality of one type is always less than or equal to the cardinality of the other, implying a total order.
More concisely: For any types `α` and `β`, there exists an injective function between them, and hence their cardinalities are comparable in a total order.
|
Function.Embedding.antisymm
theorem Function.Embedding.antisymm : ∀ {α : Type u} {β : Type v}, (α ↪ β) → (β ↪ α) → Nonempty (α ≃ β)
**The Schröder-Bernstein Theorem**: This theorem states that for any two types `α` and `β`, if there are embeddings from `α` to `β` and vice versa, there must exist an equivalence (bijection) between `α` and `β`. In other words, if `α` and `β` can be embedded into each other, they have the same cardinality.
More concisely: If there exist injective functions from types `α` to `β` and vice versa, then there exists a bijection between `α` and `β`.
|
Function.Embedding.min_injective
theorem Function.Embedding.min_injective :
∀ {ι : Type u} (β : ι → Type v) [I : Nonempty ι], ∃ i, Nonempty ((j : ι) → β i ↪ β j)
The theorem `Function.Embedding.min_injective` states that the cardinals are well-ordered. In other words, for any given set of cardinalities (represented as a type-indexed family of types `β : ι → Type v`), where the index type `ι` is nonempty, there exists an index `i` such that for every `j`, there is an injective function from `β i` to `β j`. This means there is an element in the set of cardinals that maps injectively into the others, confirming our assertion about the well-ordering of cardinals.
More concisely: For any nonempty index type `ι`, there exists an index `i` such that there exists an injective function from the cardinality type `β i` to every other cardinality type `β j` in the family `β : ι → Type v`.
|
Function.Embedding.schroeder_bernstein
theorem Function.Embedding.schroeder_bernstein :
∀ {α : Type u} {β : Type v} {f : α → β} {g : β → α},
Function.Injective f → Function.Injective g → ∃ h, Function.Bijective h
**The Schröder-Bernstein Theorem**: This theorem asserts that if you have two sets, `α` and `β`, and you have injective (one-to-one) functions `f` from `α` to `β` and `g` from `β` to `α`, then there exists a bijective (one-to-one and onto) function `h` from `α` to `β`. In other words, if you have two sets that can each be injected into the other, then there must be a way to establish a one-to-one correspondence between the elements of the two sets.
More concisely: If two sets have injective functions between them, then they are equal in size and there exists a bijective function between them.
|