uniformContinuous_const_mul — Mathlib

English

For any fixed x in R, the map y ↦ x*y is uniformly continuous.

Русский

Для фиксированного x ∈ \\mathbb{R} отображение y ↦ x*y является равномерно непрерывным.

LaTeX

$${x : \\mathbb{R}} \Rightarrow UniformContinuous( y \mapsto x*y )$$

Lean4

theorem uniformContinuous_const_mul {x : ℝ} : UniformContinuous (x * ·) :=
  uniformContinuous_of_continuousAt_zero (DistribMulAction.toAddMonoidHom ℝ x) (continuous_const_smul x).continuousAt

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