lintegral_id — Mathlib

English

Let α have the measurable singleton property. For any a ∈ α and any f: α → ℝ≥0∞, the lintegral of f with respect to the Dirac measure at a equals f(a).

Русский

Пусть α обладает свойством измеримости одиночек. Для любого a ∈ α и любого f: α → ℝ≥0∞ линегральный интеграл f по мере Дирака в a равен f(a).

LaTeX

$$$(\int^+ f(x) \, d\delta_a(x)) = f(a)$$$

Lean4

theorem lintegral_id [MeasurableSingletonClass α] {f : α → ℝ≥0∞} (a : α) : ∫⁻ a, f a ∂(@Kernel.id α mα a) = f a := by
  rw [id_apply, lintegral_dirac]

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