sum_eq_bot_iff — Mathlib

English

A finite sum equals the bottom element ⊥ if and only if at least one summand equals ⊥.

Русский

Конечная сумма равна нижнему элементу ⊥ тогда и только тогда, когда одна из слагаемых равна ⊥.

LaTeX

$$$\sum_{i\in s} f(i) = ⊥ \iff \exists i\in s,\ f(i)=⊥$$$

Lean4

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

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