uniformity_eq_symm

Mathlib.Topology.UniformSpace.Defs

URI: https://scilib.ai/kg/mathlib#uniformity_eq_symm

English

The uniformity equals its swapped image: 𝓤 α = map Prod.swap (𝓤 α).

Русский

Равномерность совпадает со своей перестановкой: 𝓤 α = map Prod.swap (𝓤 α).

LaTeX

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

Lean4

theorem uniformity_eq_symm : 𝓤 α = map Prod.swap (𝓤 α) :=
  le_antisymm uniformity_le_symm symm_le_uniformity

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru