instNeZeroENNRealCoeSetUniv

Mathlib.MeasureTheory.Measure.MeasureSpace

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv

English

If μ is nonzero, then μ(univ) > 0, i.e. NeZero(μ(univ)).

Русский

Если μ ≠ 0, то μ(univ) > 0, т.е. NeZero(μ(univ)).

LaTeX

$$[NeZero μ] ⇒ NeZero (μ univ)$$

Lean4

instance [NeZero μ] : NeZero (μ univ) :=
  ⟨measure_univ_ne_zero.2 <| NeZero.ne μ⟩

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

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

Разделы

Аффилиация

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