measure_singleton_lt_top

Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

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

← MathLib Explorer

English

For any a, the measure of the singleton {a} is finite under a sigma-finite measure μ.

Русский

Для любого точки a мера множества {a} конечна при сигма-конечной мере μ.

LaTeX

$$$\mu\{a\} < \infty$$$

Lean4

theorem measure_singleton_lt_top [SigmaFinite μ] : μ { a } < ∞ :=
  measure_lt_top_mono (singleton_subset_iff.2 <| mem_spanningSetsIndex ..) (measure_spanningSets_lt_top _ _)

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

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

Разделы

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

Аффилиация

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