uniformity_inv_iff — Mathlib

English

For any f : ι → α × α, Tendsto f l (𝓤 α) is equivalent to Tendsto f⁻¹ l (𝓤 α).

Русский

Для любого f: ι → α × α равносильность: Tendsto f l (𝓤 α) эквивалентно Tendsto f⁻¹ l (𝓤 α).

LaTeX

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

Lean4

@[to_additive]
theorem uniformity_inv_iff {ι : Type*} {f : ι → α × α} {l : Filter ι} : Tendsto (f⁻¹) l (𝓤 α) ↔ Tendsto f l (𝓤 α) :=
  ⟨fun H ↦ inv_inv f ▸ H.uniformity_inv, Filter.Tendsto.uniformity_inv⟩

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