toFiniteMeasure_nonzero

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

English

For any probability measure μ on Ω, μ.toFiniteMeasure ≠ 0.

Русский

Для любой вероятности μ на Ω, μ.toFiniteMeasure ≠ 0.

LaTeX

$$$\\mu^{\\mathrm{toFiniteMeasure}} \\neq 0$$$

Lean4

theorem toFiniteMeasure_nonzero (μ : ProbabilityMeasure Ω) : μ.toFiniteMeasure ≠ 0 := by
  simp [← FiniteMeasure.mass_nonzero_iff]

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

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

Разделы

Аффилиация

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