uniformContinuous_mul_right' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem uniformContinuous_mul_right' [UniformContinuousConstSMul Rᵐᵒᵖ R] (a : R) :
    UniformContinuous fun b : R => b * a :=
  uniformContinuous_id.mul_const' _

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