extend_empty — Mathlib

English

The induced outer measure μ on α is defined as OuterMeasure.ofFunction(extend m) with the extension of empty set zero; i.e., μ = OuterMeasure.ofFunction(extend m, extend_empty P0 m0).

Русский

Индуцированная внешняя мера μ на α задаётся как OuterMeasure.ofFunction(extend m) совместно с нулевой мерой пустого множества; то есть μ = OuterMeasure.ofFunction(extend m, extend_empty P0 m0).

LaTeX

$$$\\mathrm{inducedOuterMeasure} = \\mathrm{OuterMeasure.ofFunction}(\\mathrm{extend}\\, m)(\\mathrm{extend\\_empty}\\; P0\\; m0)$$$

Lean4

theorem extend_empty : extend m ∅ = 0 :=
  (extend_eq _ P0).trans m0

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