instFunLikeSetENNReal — Mathlib

English

There is a canonical way to regard an outer measure on α as a function from sets to extended nonnegative reals, via its measureOn function; this presentation treats outer measures as function-like objects on the power set.

Русский

Существует каноничный способ рассматривать внешнюю меру на α как функцию от подмножеств к числам в \\mathbb{R}_{\\ge 0, \\infty}, через соответствующую функцию measureOn; внешние меры выступают как функции-объекты на множества.

LaTeX

$$$\mathrm{FunLike}(\\mathrm{OuterMeasure}\\; \\alpha)(\\mathrm{Set}\\; \\alpha)\\; \\mathbb{R}_{\\ge 0, \\infty}$ и coe m := m.\\mathrm{measureOf}$$$

Lean4

instance : FunLike (OuterMeasure α) (Set α) ℝ≥0∞
    where
  coe m := m.measureOf
  coe_injective'
    | ⟨_, _, _, _⟩, ⟨_, _, _, _⟩, rfl => rfl

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