lintegral_const — Mathlib

English

The lintegral of a constant function is the constant times the measure of the whole space.

Русский

Линтеграл константы c над μ равен c · μ(вся пространство).

LaTeX

$$$$ \int^- x, c \partial \mu = c \cdot \mu(\mathrm{univ}). $$$$

Lean4

@[simp]
theorem lintegral_const (c : ℝ≥0∞) : ∫⁻ _, c ∂μ = c * μ univ :=
  by
  rw [← SimpleFunc.const_lintegral, ← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_const]
  rfl

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