add_left — Mathlib

English

A simp lemma regarding Lebesgue decomposition sum_left.

Русский

Лемма упрощения о суммировании разложения Лебега.

LaTeX

$$Eq ((μ.singularPart ν).MutuallySingular ν) True$$

Lean4

instance add_left {μ' : Measure α} [HaveLebesgueDecomposition μ ν] [HaveLebesgueDecomposition μ' ν] :
    HaveLebesgueDecomposition (μ + μ') ν :=
  by
  have : ∀ b, HaveLebesgueDecomposition (cond b μ μ') ν := by simp [*]
  simpa using sum_left (cond · μ μ')

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