average — Mathlib

English

If μ is finite and R-scalar towers hold, then r • μ is finite for all r ∈ R.

Русский

Если μ конечна и выполняются каскады скаляров между R, NNReal и ENNReal, то для любого r ∈ R масса r • μ конечна.

LaTeX

$$IsFiniteMeasure (instHSMul.hSMul r μ)$$

Lean4

instance average : IsFiniteMeasure ((μ univ)⁻¹ • μ) where
  measure_univ_lt_top := by
    rw [smul_apply, smul_eq_mul, ← ENNReal.div_eq_inv_mul]
    exact ENNReal.div_self_le_one.trans_lt ENNReal.one_lt_top

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