restrict_singleton — Mathlib

English

The restriction of μ to a singleton {a} equals μ({a}) times the Dirac measure at a.

Русский

Ограничение меры μ до множества {a} равно μ({a}) умножить на меру Дирака в a.

LaTeX

$$$ \\mu.restrict{ a } = μ{ a } \\cdot dirac a $$$

Lean4

@[simp]
theorem restrict_singleton (μ : Measure α) (a : α) : μ.restrict { a } = μ { a } • dirac a :=
  by
  ext1 s hs
  by_cases ha : a ∈ s
  · have : s ∩ { a } = { a } := by simpa
    simp [*]
  · have : s ∩ { a } = ∅ := inter_singleton_eq_empty.2 ha
    simp [*]

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