restrict_const_lintegral — Mathlib

English

A restricted constant simple function has lintegral equal to the constant times the restricted measure of the set.

Русский

Ограниченная константная простая функция имеет линеграль равный константе, умноженной на меру ограниченного множества.

LaTeX

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

Lean4

theorem restrict_const_lintegral (c : ℝ≥0∞) {s : Set α} (hs : MeasurableSet s) :
    ((const α c).restrict s).lintegral μ = c * μ s := by
  rw [restrict_lintegral_eq_lintegral_restrict _ hs, const_lintegral_restrict]

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