measure_toMeasurable — Mathlib

English

The measure of the hull equals the measure of the original set: μ(toMeasurable μ s) = μ(s).

Русский

Мера оболочки равна мере исходного множества: μ(toMeasurable μ s) = μ(s).

LaTeX

$$μ(\mathrm{toMeasurable}(μ,s)) = μ(s)$$

Lean4

@[simp]
theorem measure_toMeasurable (s : Set α) : μ (toMeasurable μ s) = μ s :=
  by
  rw [toMeasurable_def]; split_ifs with hs h's
  · exact measure_congr hs.choose_spec.2.2
  · simpa only [inter_univ] using h's.choose_spec.2.2 univ MeasurableSet.univ
  · exact (exists_measurable_superset μ s).choose_spec.2.2

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