coeFn_univ_ne_zero

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.coeFn_univ_ne_zero

English

The total mass ν(univ) is nonzero: ν(univ) ≠ 0.

Русский

Общая масса ν(Ω) не ноль: ν(univ) ≠ 0.

LaTeX

$$ν(\\mathrm{univ}) \\ne 0$$

Lean4

theorem coeFn_univ_ne_zero (ν : ProbabilityMeasure Ω) : ν univ ≠ 0 := by
  simp only [coeFn_univ, Ne, one_ne_zero, not_false_iff]

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

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

Разделы

Аффилиация

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