count_real_singleton

Mathlib.MeasureTheory.Measure.Count

URI: https://scilib.ai/kg/mathlib#MeasureTheory.count_real_singleton

← MathLib Explorer

English

For any a, the real-valued counting measure of the singleton {a} is 1.

Русский

Для любого a выполнено: реальная счётная мера множества {a} равна 1.

LaTeX

$$$\operatorname{count.real}(\{a\}) = 1$$$

Lean4

theorem _root_.MeasureTheory.count_real_singleton [MeasurableSingletonClass α] (a : α) :
    count.real ({ a } : Set α) = 1 :=
  count_real_singleton' (measurableSet_singleton a)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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