mk — Mathlib · SciLib

English

If f is almost everywhere measurable with respect to the sum of measures m, then map f of the sum equals the sum of maps of each m i.

Русский

Если f а.е.-измерима относительно суммы мер m, тогда map f суммы равна сумме отображений map f каждой m i.

LaTeX

$$$\mathrm{map}\, f\ (\mathrm{sum}\ m) = \mathrm{sum}\ (\lambda i, \mathrm{map}\, f\ (m\ i))$$$

Lean4

theorem mk (h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0) : μ ≪ ν :=
  by
  intro s hs
  rcases exists_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩
  exact measure_mono_null h1t (h h2t h3t)

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