coe_toLargerSpace_eq — Mathlib

English

The integral of a simple function equals the finite/range sum of its values times the measure of preimages.

Русский

Интеграл простой функции равен конечной сумме значений функции, взвешенной мерами предобразов.

LaTeX

$$$\\displaystyle \\int f \\, d\\mu = \\sum_{x} a_x \\mu(f^{-1}(x))$$$

Lean4

theorem coe_toLargerSpace_eq (hm : m ≤ m0) (f : @SimpleFunc β m γ) : ⇑(f.toLargerSpace hm) = f :=
  rfl

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