English
For any α, β, either there is an embedding α ↪ β or β ↪ α.
Русский
Для любых множеств кардиналов либо существует вложение α ↪ β, либо β ↪ α.
LaTeX
$$$\text{Nonempty}(\alpha \hookrightarrow \beta) \lor \text{Nonempty}(\beta \hookrightarrow \alpha)$$$
Lean4
/-- The cardinals are totally ordered. See
`Cardinal.conditionallyCompleteLinearOrderBot` for (one of) the lattice
instance. -/
theorem total (α : Type u) (β : Type v) : Nonempty (α ↪ β) ∨ Nonempty (β ↪ α) :=
match @min_injective Bool (fun b => cond b (ULift α) (ULift.{max u v, v} β)) ⟨true⟩ with
| ⟨true, ⟨h⟩⟩ =>
let ⟨f, hf⟩ := h false
Or.inl ⟨Embedding.congr Equiv.ulift Equiv.ulift ⟨f, hf⟩⟩
| ⟨false, ⟨h⟩⟩ =>
let ⟨f, hf⟩ := h true
Or.inr ⟨Embedding.congr Equiv.ulift Equiv.ulift ⟨f, hf⟩⟩
