lintegral_const — Mathlib

English

For any f: β → ℝ≥0∞ and μ a measure on β, and a ∈ α, the lintegral with respect to const α μ at a equals the lintegral with respect to μ.

Русский

Для любого f: β → ℝ≥0∞ и меры μ на β, и для фиксированного a ∈ α, линтеграл по константному ядру равен линегралу по μ.

LaTeX

$$$\operatorname{lintegral} f \, d(\text{const } α μ)(a) = \operatorname{lintegral} f \, d μ$$$

Lean4

@[simp]
theorem lintegral_const {f : β → ℝ≥0∞} {μ : Measure β} {a : α} : ∫⁻ x, f x ∂const α μ a = ∫⁻ x, f x ∂μ := by
  rw [const_apply]

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