boundedBy_measure — Mathlib

English

The boundedBy construction of a measure equals the original outer measure: OuterMeasure.boundedBy μ = μ.toOuterMeasure.

Русский

Построение boundedBy меры равно исходной внешней мере: OuterMeasure.boundedBy μ = μ.toOuterMeasure.

LaTeX

$$$$ \mathrm{OuterMeasure}.boundedBy(\mu) = \mu^{\,\mathrm{toOuterMeasure}}. $$$$

Lean4

@[simp]
theorem boundedBy_measure (μ : Measure α) : OuterMeasure.boundedBy μ = μ.toOuterMeasure :=
  μ.toOuterMeasure.boundedBy_eq_self

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