smul — Mathlib

English

If μ is inner regular, then c • μ is inner regular for any scalar c ≥ 0, i.e., inner regularity is preserved under positive scalar multiplication.

Русский

Если μ — внутренняя регулярность, то для любого коэффициента c ≥ 0 выражение c • μ сохраняет внутреннюю регулярность.

LaTeX

$$$\\forall c\\in[0,\\infty], InnerRegular μ \\Rightarrow InnerRegular (c\\cdot μ)$$$

Lean4

instance smul [h : InnerRegular μ] (c : ℝ≥0∞) : InnerRegular (c • μ) :=
  ⟨InnerRegularWRT.smul h.innerRegular c⟩

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