uniformity_eq

Mathlib.Topology.UniformSpace.Separation

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

English

The canonical map mk is uniformly continuous from α to SeparationQuotient α.

Русский

Каноническое отображение mk из α в SeparationQuotient α равномерно непрерывно.

LaTeX

$$$UniformContinuous\ (mk: α \to SeparationQuotient(α))$$$

Lean4

theorem uniformity_eq : 𝓤 (SeparationQuotient α) = (𝓤 α).map (Prod.map mk mk) :=
  rfl

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

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

Разделы

Аффилиация

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