sum_eq_top — Mathlib

English

A finite sum of WithTop elements is equal to top if and only if at least one summand is top.

Русский

Пусть сумма конечна над WithTop; она равна верхнему элементу тогда и только тогда, когда один из слагаемых равен верхнему элементу.

LaTeX

$$$$ \sum_{i \in s} f(i) = \top \quad \iff \quad \exists i \in s,\ f(i) = \top. $$$$

Lean4

/-- A sum is infinite iff one term is infinite. -/
@[simp]
theorem sum_eq_top : ∑ i ∈ s, f i = ⊤ ↔ ∃ i ∈ s, f i = ⊤ := by induction s using Finset.cons_induction <;> simp [*]

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