measureReal_eq_coe_coeFn

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

← MathLib Explorer

English

The real-valued measure built from ν agrees with the NNReal-valued evaluation: (ν : Measure Ω).real s = ν s.

Русский

Реальная мера совпадает с NNReal-оценкой: (ν : Measure Ω).real s = ν s.

LaTeX

$$ (ν : Measure Ω).real(s) = ν(s)$$

Lean4

@[simp]
theorem measureReal_eq_coe_coeFn (ν : ProbabilityMeasure Ω) (s : Set Ω) : (ν : Measure Ω).real s = ν s := by
  simp [coeFn_def, Measure.real, ENNReal.toReal]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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