count_singleton

Mathlib.MeasureTheory.Measure.Count

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

English

If a is any element of α and the singleton {a} is measurable, then count({a}) = 1.

Русский

Пусть a — произвольный элемент, и множество {a} измеримо; тогда count({a}) = 1.

LaTeX

$$$count\,{\{a\}} = 1$$$

Lean4

theorem count_singleton [MeasurableSingletonClass α] (a : α) : count ({ a } : Set α) = 1 :=
  count_singleton' (measurableSet_singleton a)

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

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

Разделы

Аффилиация

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