ennreal_mass

Mathlib.MeasureTheory.Measure.FiniteMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.FiniteMeasure.ennreal_mass

English

If s is open and μ is positive on open sets, then s is everywhere positive.

Русский

Если s открыто и μ положительна на открытых множествах, то s повсюду положительно.

LaTeX

$$IsOpen s → IsEverywherePos μ s$$

Lean4

@[simp]
theorem ennreal_mass {μ : FiniteMeasure Ω} : (μ.mass : ℝ≥0∞) = (μ : Measure Ω) univ :=
  ennreal_coeFn_eq_coeFn_toMeasure μ Set.univ

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

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

Разделы

Аффилиация

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