restrict_dirac' — Mathlib

English

For measurable s, and a decidable predicate a ∈ s, the restriction of dirac a to s equals dirac a if a ∈ s, otherwise 0.

Русский

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

LaTeX

$$$ (dirac a).restrict s = if a \\in s then dirac a else 0 $$$

Lean4

theorem restrict_dirac' (hs : MeasurableSet s) [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
    rw [ae_dirac_iff] <;> assumption
  · rw [restrict_eq_zero, dirac_apply' _ hs, indicator_of_notMem has]

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