lintegral_singleton' — Mathlib

English

For any measurable function f, the integral over a singleton {a} equals f(a) times the measure of {a}.

Русский

Для измеримой функции f интеграл по множества {a} равен f(a) умноженному на μ({a}).

LaTeX

$$$\int_{\{a\}} f(x) \, d\mu = f(a) \mu\{a\}$$$

Lean4

theorem lintegral_singleton' {f : α → ℝ≥0∞} (hf : Measurable f) (a : α) : ∫⁻ x in { a }, f x ∂μ = f a * μ { a } := by
  simp [lintegral_dirac' _ hf, mul_comm]

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