uniformity_le_symm — Mathlib

English

The comap of the swap map on the uniformity equals the uniformity itself: comap (Prod.swap) (𝓤 α) = 𝓤 α.

Русский

Обратное образование отображения перестановки координат по униформности совпадает с самой униформностью.

LaTeX

$$$$\\mathrm{comap} (\\mathrm{Prod.swap}) (𝓤 α) = 𝓤 α.$$$$

Lean4

theorem uniformity_le_symm : 𝓤 α ≤ map Prod.swap (𝓤 α) := by rw [map_swap_eq_comap_swap];
  exact tendsto_swap_uniformity.le_comap

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