lintegral_dirac — Mathlib

English

For a fixed a and f, and a measurable set s, the integral over s of f with respect to dirac a equals f(a) if a ∈ s and 0 otherwise.

Русский

Для фиксированного a и функции f, по множеству s интеграл по dirac a равен f(a) если a ∈ s и 0 иначе.

LaTeX

$$$$\\int_{a\\in s} f(a) \\, d\\delta_a = \\begin{cases} f(a), & a\\in s \\\\ 0, & a\\notin s \\end{cases}.$$$$

Lean4

@[simp]
theorem lintegral_dirac [MeasurableSingletonClass α] (a : α) (f : α → ℝ≥0∞) : ∫⁻ a, f a ∂dirac a = f a := by
  simp [lintegral_congr_ae (ae_eq_dirac f)]

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