integral_unique — Mathlib

English

If α has a unique element, then the integral of any f is μ.real univ times f default, i.e., the integral equals the weighted constant function.

Русский

Если α имеет единственный элемент, интеграл равен μ.real univ умножить на этот элемент по умолчанию.

LaTeX

$$$\\displaystyle \\int_{\\alpha} f(a) \\, d\\mu = \\mu_{\\mathbb{R}}(\\text{univ}) \\cdot f(\\text{default})$$$

Lean4

theorem integral_unique [Unique α] (f : α → E) : ∫ x, f x ∂μ = μ.real univ • f default :=
  calc
    ∫ x, f x ∂μ = ∫ _, f default ∂μ := by congr with x; congr; exact Unique.uniq _ x
    _ = μ.real univ • f default := by rw [integral_const]

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