count_apply

Mathlib.MeasureTheory.Measure.Count

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

English

For measurable s, count s equals encard of s, when translated to measure values.

Русский

Для измеримого s, count s равно encard(s) при отображении в меры.

LaTeX

$$$$\\mathrm{count}(s) = s.encard.$$$$

Lean4

theorem count_apply (hs : MeasurableSet s) : count s = s.encard := by simp [count, hs, ← tsum_subtype]

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

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

Разделы

Аффилиация

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