sup'_eq_zero — Mathlib

English

For a nonempty finite set s and a function f: s → α, the specialized supremum over s with primed operation equals zero exactly when all f(i) are zero.

Русский

Для ненулевого конечного множества s и функции f: s → α, специальный верхний предел над s равен нулю тогда и только тогда, когда все значения f(i) равны нулю.

LaTeX

$$$s\,\operatorname{sup}'\, {hs} \, f = 0 \iff \forall i \in s\, (f(i) = 0)$$$

Lean4

@[simp]
theorem sup'_eq_zero (hs) : s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0 := by simp [sup'_eq_sup]

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