coeFn_def

Mathlib.MeasureTheory.Measure.ProbabilityMeasure

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

English

The evaluation map for a constructed ProbabilityMeasure ⟨μ, hμ⟩ is given by s ↦ (μ(s)).toNNReal.

Русский

Оценка для сконструированного ProbabilityMeasure ⟨μ, hμ⟩ задаётся как s ↦ (μ(s)).toNNReal.

LaTeX

$$DFunLike.coe (F := ProbabilityMeasure Ω) ⟨μ, hμ⟩ = (λ s. (μ s).toNNReal)$$

Lean4

theorem coeFn_def (μ : ProbabilityMeasure Ω) : μ = fun s ↦ ((μ : Measure Ω) s).toNNReal :=
  rfl

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

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

Разделы

Аффилиация

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