iSup — Mathlib

English

If every f(i) is principal, then the supremum iSup f is principal: Principal op (iSup i f).

Русский

Если каждый f(i) является principal, то их надмножество iSup тоже principal: Principal op (iSup i f).

LaTeX

$$$$ \forall {f : ι \to Ordinal}, ( \forall i, \operatorname{Principal}(op) (f i) ) \Rightarrow \operatorname{Principal}(op) (\iSup i, f i). $$$$

Lean4

protected theorem iSup {ι} {f : ι → Ordinal} (H : ∀ i, Principal op (f i)) : Principal op (⨆ i, f i) :=
  Principal.sSup (by simpa)

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