English
Assume the scalar action of a normed ring R on M is bounded and continuous. Then there is an induced IsBoundedSMul on C(α, β): dist(r f, r g) ≤ |r| dist(f,g) for all f,g ∈ C(α,β).
Русский
Пусть на M действует скалярное умножение для кольца R, ограниченное и непрерывное. Тогда на C(α,β) существует индуцированное ограниченное скаляционное умножение: for f,g ∈ C(α,β) выполняется dist(r f, r g) ≤ |r| dist(f,g).
LaTeX
$$$\mathrm{dist}(r\cdot f, r\cdot g) \le |r| \cdot \mathrm{dist}(f,g).$$$
Lean4
instance {R} [Zero R] [Zero β] [PseudoMetricSpace R] [SMul R β] [IsBoundedSMul R β] : IsBoundedSMul R C(α, β)
where
dist_smul_pair' r f g := by simpa only [← dist_mkOfCompact] using dist_smul_pair r (mkOfCompact f) (mkOfCompact g)
dist_pair_smul' r₁ r₂ f := by simpa only [← dist_mkOfCompact] using dist_pair_smul r₁ r₂ (mkOfCompact f)
