div — Mathlib

English

If f,g are uniformly continuous, then the map x ↦ f(x)/g(x) is uniformly continuous.

Русский

Если f и g равномерно непрерывны, то x ↦ f(x)/g(x) равномерно непрерывна.

LaTeX

$$$\text{UniformContinuous } f \rightarrow \text{UniformContinuous } g \Rightarrow \text{UniformContinuous } x \mapsto f(x)/g(x).$$$

Lean4

@[to_additive]
theorem div [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) :
    UniformContinuous fun x => f x / g x :=
  uniformContinuous_div.comp (hf.prodMk hg)

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