measureReal_univ_pos

Mathlib.MeasureTheory.Measure.Real

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

← MathLib Explorer

English

Under finite nonzero measure, the real-valued measure of the universe is strictly positive.

Русский

При конечной ненулевой мере real-мера универсума положительна.

LaTeX

$$0 < μ.real Set.univ$$

Lean4

@[simp]
theorem measureReal_univ_pos [IsFiniteMeasure μ] [NeZero μ] : 0 < μ.real Set.univ :=
  ENNReal.toReal_pos (NeZero.ne (μ Set.univ)) (measure_ne_top μ univ)

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

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

Разделы

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

Аффилиация

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