isFiniteMeasure_toFiniteAux — Mathlib

English

For [SFinite μ], ae μ.toFinite = ae μ; the a.e. sets are identical for the finite version.

Русский

Для [SFinite μ], ae μ.toFinite = ae μ; множества почти всюду совпадают.

LaTeX

$$$ \ae μ.toFinite = \ae μ $$$

Lean4

@[local instance]
theorem isFiniteMeasure_toFiniteAux [SFinite μ] : IsFiniteMeasure μ.toFiniteAux :=
  by
  rw [Measure.toFiniteAux]
  split_ifs
  · assumption
  · exact (exists_isFiniteMeasure_absolutelyContinuous μ).choose_spec.1

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