uniformContinuous_inv — Mathlib

English

If s ⊆ ℝ avoids 0 by a margin r>0, then p ↦ p⁻¹ is uniformly continuous on s.

Русский

Если множество s⊆ℝ отстоит от нуля на величину r>0, отображение p↦p⁻¹ на s равно равномерно непрерывно.

LaTeX

$$$\forall s\subseteq\mathbb{R}, \; (\exists r>0:\forall x\in s, |x| \ge r) \Rightarrow\text{UniformContinuous}(x\mapsto x^{-1}\text{ on }s)$$$

Lean4

theorem uniformContinuous_inv (s : Set ℝ) {r : ℝ} (r0 : 0 < r) (H : ∀ x ∈ s, r ≤ |x|) :
    UniformContinuous fun p : s => p.1⁻¹ :=
  Metric.uniformContinuous_iff.2 fun _ε ε0 =>
    let ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma abs ε0 r0
    ⟨δ, δ0, fun {a b} h => Hδ (H _ a.2) (H _ b.2) h⟩

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