restrict_dirac — Mathlib

English

The Dirac delta measure at a point a, when restricted to a subset s, equals the Dirac measure at a if a lies in s, and equals the zero measure otherwise.

Русский

Дирaковa мера δ_a, ограниченная до множества s, равна δ_a при условии a ∈ s, и равна нулевой мере, если a ∉ s.

LaTeX

$$$(\\mathrm{dirac}\\ a)\\restriction s = \\begin{cases} \\mathrm{dirac}\\ a, & a \\in s \\\\ 0, & a \\notin s \\end{cases}$$$

Lean4

theorem restrict_dirac [MeasurableSingletonClass α] [Decidable (a ∈ s)] :
    (Measure.dirac a).restrict s = if a ∈ s then Measure.dirac a else 0 :=
  by
  split_ifs with has
  · apply restrict_eq_self_of_ae_mem
    rwa [ae_dirac_eq]
  · rw [restrict_eq_zero, dirac_apply, indicator_of_notMem has]

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