iSup_eq_zero — Mathlib

English

If f is bounded above, then ⨆ i, f(i) = 0 if and only if f(i) = 0 for all i.

Русский

Если значения f ограничены сверху, то ⨆ i, f(i) = 0 тогда и только тогда, когда все f(i) равны 0.

LaTeX

$$$ \mathrm{BddAbove}(\mathrm{range}(f)) \Rightarrow ( \sup_i f(i) = 0 \iff \forall i, f(i) = 0 ).$$$

Lean4

@[simp]
theorem iSup_eq_zero (hf : BddAbove (range f)) : ⨆ i, f i = 0 ↔ ∀ i, f i = 0 :=
  by
  cases isEmpty_or_nonempty ι
  · simp
  · simp [← bot_eq_zero', ← le_bot_iff, ciSup_le_iff hf]

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