iSup_typein_limit — Mathlib

English

If ho: type r = o, and a condition holds, the iSup over the typein embedding equals o.

Русский

При равенстве типа и условии, величина iSup над embedding typein равна o.

LaTeX

$$$i\!\!\sup\; \text{typein} = o$$$

Lean4

theorem iSup_typein_limit {o : Ordinal.{u}} (ho : ∀ a, a < o → succ a < o) :
    iSup (typein ((· < ·) : o.toType → o.toType → Prop)) = o :=
  by
  rw [(iSup_eq_lsub_iff.{u, u} (typein (· < ·))).2] <;> rw [lsub_typein o]
  assumption

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