sum_ne_top — Mathlib

English

The sum ∑ f i is not top if and only if every summand f i is not top.

Русский

Сумма не равна верхнему элементу тогда и только тогда, когда каждое слагаемое не равно верхнему элементу.

LaTeX

$$$$ \sum_{i \in s} f(i) \neq \top \iff \forall i \in s,\ f(i) \neq \top. $$$$

Lean4

/-- A sum is finite iff all terms are finite. -/
theorem sum_ne_top : ∑ i ∈ s, f i ≠ ⊤ ↔ ∀ i ∈ s, f i ≠ ⊤ := by simp

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