integral_singleton — Mathlib

English

Let α be such that a measurable singleton exists; for any measurable f, ∫ a in {a}, f(a) dμ = μ.real{a} · f(a).

Русский

Пусть для некоторого a существует измеримое множество {a}; тогда интеграл по {a} равен μ.real{a} · f(a).

LaTeX

$$$\\displaystyle \\int_{\\{a\\}} f(a) \\, d\\mu = \\mu_{\\mathbb{R}}(\\{a\\}) \\cdot f(a)$$$

Lean4

theorem integral_singleton [MeasurableSingletonClass α] {μ : Measure α} (f : α → E) (a : α) :
    ∫ a in { a }, f a ∂μ = μ.real { a } • f a := by
  simp only [Measure.restrict_singleton, integral_smul_measure, integral_dirac, measureReal_def]

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