measureReal_univ_ne_zero

Mathlib.MeasureTheory.Measure.Real

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

English

If μ is finite and nonzero, then μ.real of the universal set is nonzero.

Русский

Если μ конечна и не ноль, то μ.real(универсум) ≠ 0.

LaTeX

$$μ.real Set.univ ≠ 0$$

Lean4

theorem measureReal_univ_ne_zero [IsFiniteMeasure μ] [NeZero μ] : μ.real Set.univ ≠ 0 :=
  measureReal_univ_pos.ne'

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

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

Разделы

Аффилиация

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