isFiniteMeasure

Mathlib.MeasureTheory.Measure.Count

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.count.isFiniteMeasure

English

On a finite type α, the counting measure is a finite measure.

Русский

На конечном типе α счётная мера является конечной мерой.

LaTeX

$$$\text{IsFiniteMeasure}(\text{count}:\text{Measure }\alpha)$$$

Lean4

instance isFiniteMeasure [Finite α] : IsFiniteMeasure (Measure.count : Measure α) :=
  ⟨by simp [Measure.count_apply]⟩

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

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

Разделы

Аффилиация

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