iSup_eq_zero_iff — Mathlib

English

If the ranges of two ordinal-valued functions coincide, their iSup are equal.

Русский

Если диапазоны двух функций-значений порядков совпадают, их iSup равны.

LaTeX

$$$\mathrm{range}\ f = \mathrm{range}\ g \Rightarrow iSup\ f = iSup\ g$$$

Lean4

theorem iSup_eq_zero_iff {ι} {f : ι → Ordinal.{u}} [Small.{u} ι] : iSup f = 0 ↔ ∀ i, f i = 0 :=
  by
  refine ⟨fun h i => ?_, fun h => le_antisymm (Ordinal.iSup_le fun i => Ordinal.le_zero.2 (h i)) (Ordinal.zero_le _)⟩
  rw [← Ordinal.le_zero, ← h]
  exact Ordinal.le_iSup f i

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