instFunLike — Mathlib

English

There is a canonical function-like structure on FiniteMeasure Ω given by μ(s) = (μ : Measure Ω)(s) viewed in NNReal, compatible with the underlying measure.

Русский

Существует каноническая функция-подобная структура на FiniteMeasure Ω: μ(s) = (μ : Measure Ω)(s), приведённая к NNReal, совместимая с базовой мерой.

LaTeX

$$FiniteMeasure.instFunLike : FunLike (FiniteMeasure Ω) (Set Ω) NNReal$$

Lean4

instance instFunLike : FunLike (FiniteMeasure Ω) (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

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