iSup_typein_succ — Mathlib

English

Similarly, iSup over typein on (succ o) equals o.

Русский

Аналогично, iSup над typein на (succ o) равен o.

LaTeX

$$$i\sup\; (typein \; (succ\; o)) = o$$$

Lean4

@[simp]
theorem iSup_typein_succ {o : Ordinal} : iSup (typein ((· < ·) : (succ o).toType → (succ o).toType → Prop)) = o :=
  by
  rcases iSup_eq_lsub_or_succ_iSup_eq_lsub (typein ((· < ·) : (succ o).toType → (succ o).toType → Prop)) with h | h
  · rw [iSup_eq_lsub_iff] at h
    simp only [lsub_typein] at h
    exact (h o (lt_succ o)).false.elim
  rw [← succ_eq_succ_iff, h]
  apply lsub_typein

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