lintegral_deterministic — Mathlib

English

Non-kernel version: for measurable g and measurable f, ∫⁻ f ∂deterministic g hg a = f(g(a)).

Русский

Нетипично для ядра: линтеграл по детерминированному отображению дает значение f(g(a)).

LaTeX

$$$\int⁻ f \partial\deterministic g hg a = f(g(a))$$$

Lean4

@[simp]
theorem lintegral_deterministic {f : β → ℝ≥0∞} {g : α → β} {a : α} (hg : Measurable g) [MeasurableSingletonClass β] :
    ∫⁻ x, f x ∂deterministic g hg a = f (g a) := by rw [deterministic_apply, lintegral_dirac (g a) f]

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