bsup_eq_zero_iff — Mathlib

English

The supremum bsup o f is zero exactly when every f i hi is zero.

Русский

Наибольший элемент bsup o f равен нулю тогда и только тогда, когда каждый f(i,h) равен нулю.

LaTeX

$$$\\operatorname{bsup}(o,f) = 0 \\iff \\forall i\\, hi,\\ f(i,hi) = 0$$$

Lean4

@[simp]
theorem bsup_eq_zero_iff {o} {f : ∀ a < o, Ordinal} : bsup o f = 0 ↔ ∀ i hi, f i hi = 0 :=
  by
  refine ⟨fun h i hi => ?_, fun h => le_antisymm (bsup_le fun i hi => Ordinal.le_zero.2 (h i hi)) (Ordinal.zero_le _)⟩
  rw [← Ordinal.le_zero, ← h]
  exact le_bsup f i hi

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