English
Cardinals with addition form a canonically ordered additive structure.
Русский
Кардинальные числа с операцией сложения образуют канонически упорядоченную добавочную структуру.
LaTeX
$$$\text{CanonicallyOrderedAdd}(\mathrm{Cardinal})$$$
Lean4
instance canonicallyOrderedAdd : CanonicallyOrderedAdd Cardinal.{u}
where
exists_add_of_le
{a
b} :=
inductionOn₂ a b fun α β ⟨⟨f, hf⟩⟩ =>
have : α ⊕ ((range f)ᶜ : Set β) ≃ β := by
classical exact (Equiv.sumCongr (Equiv.ofInjective f hf) (Equiv.refl _)).trans <| Equiv.Set.sumCompl (range f)
⟨#(↥(range f)ᶜ), mk_congr this.symm⟩
le_self_add a _ := (add_zero a).ge.trans <| add_le_add_left (Cardinal.zero_le _) _
le_add_self a _ := (zero_add a).ge.trans <| add_le_add_right (Cardinal.zero_le _) _
