toOuterMeasure_toMeasure — Mathlib

English

For any measure μ on α, converting μ to an outer measure and back recovers μ: μ.toOuterMeasure.toMeasure (le_toOuterMeasure_caratheodory _) = μ.

Русский

Для любой меры μ на α преобразование μ в внешнюю меру и обратное преобразование восстанавливают μ: μ.toOuterMeasure.toMeasure (le_toOuterMeasure_caratheodory _) = μ.

LaTeX

$$$\\mu.toOuterMeasure.toMeasure (le\\_toOuterMeasure\\_caratheodory _) = \\mu$$$

Lean4

@[simp]
theorem toOuterMeasure_toMeasure {μ : Measure α} : μ.toOuterMeasure.toMeasure (le_toOuterMeasure_caratheodory _) = μ :=
  Measure.ext fun _s => μ.toOuterMeasure.trim_eq

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