mul_const — Mathlib

English

If f: β → α is uniformly continuous and a ∈ α is fixed, then the map x ↦ f(x) · a is uniformly continuous.

Русский

Если f: β → α равномерно непрерывна и фиксировано выбрано a ∈ α, то отображение x ↦ f(x) · a равномерно непрерывно.

LaTeX

$$$\\mathrm{Uniformly\\;continuous}(f) \\rightarrow \\forall a \\in \\alpha,\\ \\mathrm{Uniformly\\;continuous}(x \\mapsto f(x) \\cdot a)$$$

Lean4

@[to_additive]
theorem mul_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) (a : α) : UniformContinuous fun x ↦ f x * a :=
  hf.mul uniformContinuous_const

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