mutuallySingular_dirac — Mathlib

English

If a measure μ on α has no atoms, then the Dirac measure at any point x is mutually singular with μ.

Русский

Если мера μ на α не имеет атомов, то мера Дирака δ_x и μ взаимно-сингулярны.

LaTeX

$$$\\mathrm{dirac}_x \\perp_m \\mu$$$

Lean4

theorem mutuallySingular_dirac [MeasurableSingletonClass α] (x : α) (μ : Measure α) [NoAtoms μ] :
    Measure.dirac x ⟂ₘ μ :=
  ⟨{ x }ᶜ, (MeasurableSet.singleton x).compl, by simp, by simp⟩

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