integral_const — Mathlib

English

The integral of a function with respect to a constant kernel equals the integral with respect to the base measure.

Русский

Интеграл функции по константному ядру равен интегралу по исходной мере.

LaTeX

$$$\\int x, f(x) \\, d\\mathrm{const}(\\alpha, \\mu) = \\int x, f(x) \\, d\\mu$$$

Lean4

@[simp]
theorem integral_const {μ : Measure β} : ∫ x, f x ∂const α μ a = ∫ x, f x ∂μ := by rw [const_apply]

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