setLIntegral_const — Mathlib

English

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

Русский

Для любого f: β → ℝ≥0∞, меры μ, a ∈ α и измеримого множества s ⊆ β, линеральный интеграл по ограниченной константной мерe равен ограниченному линегралу по μ.

LaTeX

$$$\int^+_{x \in s} f(x) \, d(\text{const } α μ)(a) = \int^+_{x \in s} f(x) \, d μ(x)$$$

Lean4

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

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