mk_apply — Mathlib

English

For any μ and hμ that define a ProbabilityMeasure, the value at s is (μ(s)).toNNReal.

Русский

Для любого μ и hμ, задающих ProbabilityMeasure, значение в s равно (μ(s)).toNNReal.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem mk_apply (μ : Measure Ω) (hμ) (s : Set Ω) :
    DFunLike.coe (F := ProbabilityMeasure Ω) ⟨μ, hμ⟩ s = (μ s).toNNReal :=
  rfl

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