smul_nnreal — Mathlib

English

The finiteness on compacts is preserved under multiplication by NNReal scalars.

Русский

Финитность на компактных сохраняется под умножением на скаляры NNReal.

LaTeX

$$$\forall c\in NNReal,\ IsFiniteMeasureOnCompacts (c \cdot \mu)$$$

Lean4

instance smul_nnreal [TopologicalSpace α] (μ : Measure α) [IsFiniteMeasureOnCompacts μ] (c : ℝ≥0) :
    IsFiniteMeasureOnCompacts (c • μ) :=
  IsFiniteMeasureOnCompacts.smul μ coe_ne_top

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