instFunLike — Mathlib

English

A probability measure acts like a function on sets, with its values in NNReal; i.e., the evaluation map μ ↦ (s ↦ μ(s)) is a function-like object into NNReal.

Русский

Распределение ведёт себя как функция на множествах, принимая значения в NNReal; отображение μ ↦ (s ↦ μ(s)) образует функциональный объект в NNReal.

LaTeX

$$∀ μ, s, μ(s) = ((μ : Measure Ω)(s)).toNNReal$$

Lean4

instance instFunLike : FunLike (ProbabilityMeasure Ω) (Set Ω) ℝ≥0
    where
  coe μ s := ((μ : Measure Ω) s).toNNReal
  coe_injective' μ ν
    h :=
    toMeasure_injective <|
      Measure.ext fun s _ ↦ by simpa [ENNReal.toNNReal_eq_toNNReal_iff, measure_ne_top] using congr_fun h s

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