tsum_set_const

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

English

For c ∈ ENNReal and a set s, the sum over s of c equals encard(s) times c.

Русский

Для c ∈ ENNReal и множества s сумма по s от c равна encard(s) умножить на c.

LaTeX

$$$\sum'_{x \in s} c = s.encard \cdot c$$

Lean4

theorem tsum_set_const (c : ℝ≥0∞) : ∑' _ : s, c = s.encard * c := by simp [← tsum_set_one, ← ENNReal.tsum_mul_right]

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

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

Разделы

Аффилиация

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