iSup_succ — Mathlib

English

Let o be an ordinal. Then the supremum over all a < o of the successor of a equals o.

Русский

Пусть o — ординал. Тогда супремум по всем a < o от successor(a) равен o.

LaTeX

$$$$ \\sup_{a < o} \\operatorname{succ}(a) = o $$$$

Lean4

theorem iSup_succ (o : Ordinal) : ⨆ a : Iio o, succ a.1 = o :=
  by
  apply (le_of_forall_lt _).antisymm'
  · simp [Ordinal.iSup_le_iff]
  ·
    exact fun a ha ↦
      (lt_succ a).trans_le <|
        Ordinal.le_iSup (fun x : Iio _ ↦ _)
          ⟨a, ha⟩
            -- TODO: generalize to conditionally complete lattices

Похожие утверждения