sum_lt_bot — Mathlib

English

A finite sum is strictly above bottom provided each summand is not bottom.

Русский

Конечная сумма больше ⊥, если каждый член суммы не равен ⊥.

LaTeX

$$$\forall i\in s,\ f(i) \neq ⊥ \Rightarrow ⊥ < \sum_{i\in s} f(i)$$$

Lean4

/-- A sum of finite terms is finite. -/
theorem sum_lt_bot (h : ∀ i ∈ s, f i ≠ ⊥) : ⊥ < ∑ i ∈ s, f i :=
  bot_lt_sum_iff.2 fun i hi ↦ WithBot.bot_lt_iff_ne_bot.2 (h i hi)

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