toUniformContinuousConstSMul — Mathlib

English

The distance after multiplying by the same y on the right is controlled by the distance in the left factor.

Русский

Расстояние после умножения с одной стороны на одно и то же y контролируется расстоянием между левые множители.

LaTeX

$$dist(x1•y, x2•y) ≤ dist(x1,x2) · dist(y,0)$$

Lean4

instance (priority := 100) toUniformContinuousConstSMul : UniformContinuousConstSMul α β :=
  ⟨fun c => ((lipschitzWith_iff_dist_le_mul (K := nndist c 0)).2 fun _ _ => dist_smul_pair c _ _).uniformContinuous⟩
    -- this instance could be deduced from `NormedSpace.isBoundedSMul`, but we prove it separately
    -- here so that it is available earlier in the hierarchy

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