setIntegral_const — Mathlib

English

Restricting the integral of a function to a set s with a constant kernel equals the restricted integral with respect to μ.

Русский

Ограничение интеграла к множеству s для константного ядра эквивалентно ограниченному интегралу по μ.

LaTeX

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

Lean4

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

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