inv — Mathlib

English

If f is uniformly continuous, then the map x ↦ f(x)⁻¹ is uniformly continuous.

Русский

Если f равномерно непрерывна, то отображение x ↦ f(x)^{-1} равномерно непрерывно.

LaTeX

$$$\text{UniformContinuous } f \Rightarrow \text{UniformContinuous } x \mapsto (f(x))^{-1}$$$

Lean4

@[to_additive]
theorem inv [UniformSpace β] {f : β → α} (hf : UniformContinuous f) : UniformContinuous fun x => (f x)⁻¹ :=
  by
  have : UniformContinuous fun x => 1 / f x := uniformContinuous_const.div hf
  simp_all

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