comap_mk_uniformity

Mathlib.Topology.UniformSpace.Separation

URI: https://scilib.ai/kg/mathlib#SeparationQuotient.comap_mk_uniformity

English

The comap of the pushforward of the uniformity along mk equals the original uniformity on α.

Русский

Комап отображения mk, применённый к образованию по mk от 𝓤 α, возвращает исходную 𝓤 α.

LaTeX

$$$(\mathcal{U}(α)).comap (Prod.map mk mk) = 𝓤 α$$$

Lean4

theorem comap_mk_uniformity : (𝓤 (SeparationQuotient α)).comap (Prod.map mk mk) = 𝓤 α :=
  comap_map_mk_uniformity

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

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

Разделы

Аффилиация

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