div_const — Mathlib

English

If f: β → α is uniformly continuous, then the map x ↦ f(x) / a is uniformly continuous for any a ∈ α.

Русский

Если f: β → α равномерно непрерывна, то отображение x ↦ f(x) / a равно равномерно непрерывному для любого a ∈ α.

LaTeX

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

Lean4

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

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