lintegral_singleton

Mathlib.MeasureTheory.Integral.Lebesgue.Countable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.lintegral_singleton

English

Under a countable-singleton framework, the lintegral over {a} equals f(a) times μ({a}).

Русский

В рамках счётной меры по множества {a} интеграл равен f(a) умноженному на μ({a}).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru