div_const' — Mathlib

English

Let R be a division ring and f β → R be UniformContinuous. Then for any a ∈ R, the map x ↦ f(x)/a is UniformContinuous.

Русский

Пусть R — дивизионное кольцо, и f: β → R непрерывно-однородна. Тогда для любого a ∈ R отображение x ↦ f(x)/a равномерно непрерывно.

LaTeX

$$$\\forall a \\in R,\\; (\\text{UniformContinuous } f) \\Rightarrow \\operatorname{UniformContinuous}(x \\mapsto f(x)/a)$$$

Lean4

theorem div_const' {R β : Type*} [DivisionRing R] [UniformSpace R] [UniformContinuousConstSMul Rᵐᵒᵖ R] [UniformSpace β]
    {f : β → R} (hf : UniformContinuous f) (a : R) : UniformContinuous fun x ↦ f x / a := by
  simpa [div_eq_mul_inv] using hf.mul_const' a⁻¹

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