English
Canonical existence of a sum representation under a left-bounded relation: for ordinals, there exists a decomposition compatible with a given order embedding.
Русский
Каноническое существование представления суммы под условием левой огр. для ординалов: существует разложение, совместимое с заданной вложенной порядковой связью.
LaTeX
$$$\text{ExistsAddOfLE }\mathrm{Ordinal}$$$
Lean4
instance existsAddOfLE : ExistsAddOfLE Ordinal where
exists_add_of_le
{a b} := by
refine inductionOn₂ a b fun α r _ β s _ ⟨f⟩ ↦ ?_
obtain ⟨γ, t, _, ⟨g⟩⟩ := f.exists_sum_relIso
exact
⟨type t, g.ordinal_type_eq.symm⟩
-- TODO: This gives us `zero_le` as an immediate consequence.
-- Private/protect the old theorem, golf proofs.
