bot_lt_sum_iff — Mathlib

English

A sum is finite iff all summands are finite: ⊥ < ∑ f i iff ∀ i ∈ s, ⊥ < f i.

Русский

Сумма конечна тогда и только тогда, когда каждый слагаемое конечно: ⊥ < сумма ⇔ для всех i ∈ s, ⊥ < f(i).

LaTeX

$$$⟂ < \sum_{i\in s} f(i) \iff \forall i\in s,\ ⟂ < f(i)$$$

Lean4

/-- A sum is finite iff all terms are finite. -/
theorem bot_lt_sum_iff : ⊥ < ∑ i ∈ s, f i ↔ ∀ i ∈ s, ⊥ < f i := by
  simp only [WithBot.bot_lt_iff_ne_bot, ne_eq, sum_eq_bot_iff, not_exists, not_and]

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