op_eq_self_of_principal — Mathlib

English

If a < o, op a is normal, o is principal and a succ-lim, then op a o = o.

Русский

Если a < o, op a нормален, o — principal, и o является пределом следущего значения, то op a o = o.

LaTeX

$$$$ \forall {a o},\ \operatorname{Ordinal.partialOrder}.lt a o \Rightarrow \operatorname{IsNormal}(\operatorname{op} a) \Rightarrow \operatorname{Principal}(op)\ o \Rightarrow \operatorname{IsSuccLimit}(o) \Rightarrow \operatorname{op} a o = o. $$$$

Lean4

theorem op_eq_self_of_principal (hao : a < o) (H : IsNormal (op a)) (ho : Principal op o) (ho' : IsSuccLimit o) :
    op a o = o := by
  apply H.le_apply.antisymm'
  rw [H.apply_of_isSuccLimit ho', Ordinal.iSup_le_iff]
  exact fun ⟨b, hbo⟩ ↦ (ho hao hbo).le

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