uniformity_symm — Mathlib

English

If f maps into α × α and Tendsto f l (𝓤 α), then the coordinate-swapped function x ↦ ((f x)₂, (f x)₁) also tends to 𝓤 α.

Русский

Если f:β→α×α функционально сходится к 𝓤 α, то функция x ↦ ((f x)₂, (f x)₁) также сходится к 𝓤 α.

LaTeX

$$$$\\forall {α} [UniformSpace α] {l: Filter β} {f: β \\to α\\times α},\\;\\mathrm{Tendsto} f\\ l\\ (𝓤 α) \\Rightarrow \\mathrm{Tendsto}(x \\mapsto ((f x).2, (f x).1))\\ l\\ (𝓤 α).$$$$

Lean4

/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is symmetric. -/
theorem uniformity_symm {l : Filter β} {f : β → α × α} (h : Tendsto f l (𝓤 α)) :
    Tendsto (fun x => ((f x).2, (f x).1)) l (𝓤 α) :=
  tendsto_swap_uniformity.comp h

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