const_lintegral_restrict — Mathlib

English

Restricting a constant simple function to s gives the constant times the measure of s.

Русский

Ограничение константной простой функции на s даёт константу, умноженную на меру s.

LaTeX

$$$((\\text{const } α\\, c).\\text{restrict } s).lintegral μ = c \\cdot μ(s)$$$

Lean4

theorem const_lintegral_restrict (c : ℝ≥0∞) (s : Set α) : (const α c).lintegral (μ.restrict s) = c * μ s := by
  rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]

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