tendsto_swap_uniformity — Mathlib

English

Let α be a uniform space. The swapping map on α × α preserves the uniform structure, i.e., the swap map sends entourages to entourages; equivalently, Tendsto Prod.swap (𝓤 α) (𝓤 α).

Русский

Пусть α — равномерное пространство. Отображение перестановки координат на α × α сохраняет равномерность: для любого окружения E ∈ 𝓤 α его транспонированное окружение E^T also принадлежит 𝓤 α; эквивалентно Tendsto Prod.swap (𝓤 α) (𝓤 α).

LaTeX

$$$$\\text{Tendsto}(\\mathrm{Prod.swap})\\,(\\mathcal{U}(\\alpha))\\,(\\mathcal{U}(\\alpha)).$$$$

Lean4

theorem tendsto_swap_uniformity : Tendsto (@Prod.swap α α) (𝓤 α) (𝓤 α) :=
  symm_le_uniformity

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