uniformity_inv — Mathlib

English

If f: ι → α × α tends to the uniformity, then f⁻¹ also tends to the uniformity.

Русский

Если f: ι → α × α сходится к униформности, то и f⁻¹ сходится к униформности.

LaTeX

$$$\\mathrm{Tendsto}(f, l, 𝓤(α)) \\rightarrow \\mathrm{Tendsto}(f^{-1}, l, 𝓤(α))$$$

Lean4

@[to_additive]
theorem uniformity_inv {ι : Type*} {f : ι → α × α} {l : Filter ι} (hf : Tendsto f l (𝓤 α)) : Tendsto (f⁻¹) l (𝓤 α) :=
  have : Tendsto (·⁻¹) (𝓤 α) (𝓤 α) := uniformContinuous_inv
  this.comp hf

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