coeFn_empty

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

English

For any ν, ν(∅) = 0.

Русский

Для любого ν, ν(∅) = 0.

LaTeX

$$$ν(\\emptyset) = 0$$$

Lean4

@[simp]
theorem coeFn_empty (ν : ProbabilityMeasure Ω) : ν ∅ = 0 := by simp [coeFn_def]

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

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

Разделы

Аффилиация

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