ne_top_of_tsum_ne_top

Mathlib.Topology.Instances.ENNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#ENNReal.ne_top_of_tsum_ne_top

English

If ∑' a, f(a) ≠ ∞, then for every a, f(a) ≠ ∞.

Русский

Если сумма не бесконечна, то каждый член конечен.

LaTeX

$$$\big( \sum'_{a \in \alpha} f(a) \neq \infty \big) \rightarrow \; \forall a, f(a) \neq \infty$$$

Lean4

protected theorem ne_top_of_tsum_ne_top (h : ∑' a, f a ≠ ∞) (a : α) : f a ≠ ∞ := fun ha =>
  h <| ENNReal.tsum_eq_top_of_eq_top ⟨a, ha⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru