sup_eq_zero — Mathlib

English

For a finite index set s and a function f: s → α in a canonically ordered additive monoid with a bottom, the supremum over s is zero if and only if every f(i) = 0 for i ∈ s.

Русский

Пусть s — конечный набор индексов, а f: s → α. Тогда sup_s f = 0 тогда и только тогда, когда все значения f(i) равны 0 для i ∈ s.

LaTeX

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

Lean4

@[simp]
theorem sup_eq_zero : s.sup f = 0 ↔ ∀ i ∈ s, f i = 0 := by simp [← bot_eq_zero']

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