uniformContinuous_mul_left' — Mathlib

English

Let R be a ring with a uniform structure. For any a in R, the map b ↦ a b is uniformly continuous.

Русский

Пусть R — кольцо с равномерной структурой. Для любого a ∈ R отображение b ↦ ab равномерно непрерывно.

LaTeX

$$$\\forall a \\in R,\\; \\operatorname{UniformContinuous}(b \\mapsto a b)$$$

Lean4

theorem uniformContinuous_mul_left' [UniformContinuousConstSMul R R] (a : R) : UniformContinuous fun b : R => a * b :=
  uniformContinuous_id.const_mul' _

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