tsum_geometric_lt_top

Mathlib.Analysis.SpecificLimits.Basic

URI: https://scilib.ai/kg/mathlib#tsum_geometric_lt_top

English

If r < 1, then ∑' i r^{encode i} < ∞ for Encodable ι.

Русский

Пусть r < 1. Тогда для кодируемого множества индексов ∑' i r^{encode i} < ∞.

LaTeX

$$$$\sum_{i} r^{\mathrm{encode}(i)} < \infty \quad (r < 1).$$$$

Lean4

theorem tsum_geometric_lt_top {r : ℝ≥0∞} : ∑' n, r ^ n < ∞ ↔ r < 1 := by simp

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

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

Разделы

Аффилиация

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