tsum_one

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

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

English

The sum over the whole type α of 1 equals ENat.card α (as ENNReal).

Русский

Сумма по всем элементам α единицы равна ENat.card α (в ENNReal).

LaTeX

$$tsum_{x \in α} 1 = ENat.card α$$

Lean4

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

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

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

Разделы

Аффилиация

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