instFunLike — Mathlib

English

An instance provides an outer-measure-based function-like structure for measures: μ is a function on sets with real nonnegative values.

Русский

Экземпляр задаёт функциональность меры как отображение множеств в неотрицательные числа.

LaTeX

$$instance instFunLike [MeasurableSpace α] : FunLike (Measure α) (Set α) ENNReal$$

Lean4

instance instFunLike [MeasurableSpace α] : FunLike (Measure α) (Set α) ℝ≥0∞
    where
  coe μ := μ.toOuterMeasure
  coe_injective'
    | ⟨_, _, _⟩, ⟨_, _, _⟩, h => toOuterMeasure_injective <| DFunLike.coe_injective h

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