tsum_const

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

English

For any set α and ENNReal c, the sum over α of c equals ENNat.card α times c.

Русский

Для любого множества α и ENNReal c сумма по α от c равна ENNat.card α умножить на c.

LaTeX

$$$\sum'_{x \in α} c = (ENNat.card α) \cdot c$$

Lean4

@[simp]
theorem tsum_const (c : ℝ≥0∞) : ∑' _ : α, c = ENat.card α * c := by rw [← tsum_univ];
  simpa [encard_univ] using tsum_set_const univ c

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

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

Разделы

Аффилиация

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