sum_lt_top — Mathlib

English

For WithTop with LT structure, a finite sum is less than top iff all terms are less than top: ∑ f i < top iff ∀ i, f i < top.

Русский

Для WithTop с порядком lt: сумма меньше верхнего тогда и только тогда, когда каждое слагаемое меньше верхнего.

LaTeX

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

Lean4

/-- A sum is finite iff all terms are finite. -/
@[simp]
theorem sum_lt_top : ∑ i ∈ s, f i < ⊤ ↔ ∀ i ∈ s, f i < ⊤ := by simp [WithTop.lt_top_iff_ne_top]

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