inducedOuterMeasure — Mathlib

English

For hs : P s, the induced outer measure on s equals extend m s; i.e., the induced measure restricts to the extension.

Русский

При hs : P s индуцированная внешняя мера на s равна extend m s; индуцированная мера ограничивается расширением.

LaTeX

$$$\\mathrm{inducedOuterMeasure}\\ m\\ P0\\ m0\\ s = \\mathrm{extend}\\ m\\ s$ for hs$$

Lean4

/-- Given an arbitrary function on a subset of sets, we can define the outer measure corresponding
  to it (this is the unique maximal outer measure that is at most `m` on the domain of `m`). -/
def inducedOuterMeasure : OuterMeasure α :=
  OuterMeasure.ofFunction (extend m) (extend_empty P0 m0)

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