instTopologicalSpaceQuotient

Mathlib.Topology.DiscreteQuotient

URI: https://scilib.ai/kg/mathlib#DiscreteQuotient.instTopologicalSpaceQuotient

English

The space S is equipped with the quotient topology induced by the projection map π: X → X/∼.

Русский

Пространство S оснащено факторной топологией, полученной из отображения проекции π: X → X/~.

LaTeX

$$$ \\mathcal{T}_S = \\mathcal{T}_{\\text{quot}}(\\pi) $$$

Lean4

instance : TopologicalSpace S :=
  inferInstanceAs (TopologicalSpace (Quotient S.toSetoid))

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

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

Разделы

Аффилиация

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