lintegral_unique — Mathlib

English

For a unique-type α, the lintegral of f with respect to μ equals f(default) times μ(univ).

Русский

Для типа α с единственным элементом линтеграл по f равен f(default) умножить на μ(полное множество).

LaTeX

$$$\int_{\alpha} f(a) \, d\mu = f(\text{default}) \mu(\,\mathrm{univ}\,)$$$

Lean4

theorem lintegral_unique [Unique α] (f : α → ℝ≥0∞) : ∫⁻ x, f x ∂μ = f default * μ univ :=
  calc
    ∫⁻ x, f x ∂μ = ∫⁻ _, f default ∂μ := lintegral_congr <| Unique.forall_iff.2 rfl
    _ = f default * μ univ := lintegral_const _

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