instDiscreteTopologyQuotient

Mathlib.Topology.DiscreteQuotient

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

← MathLib Explorer

English

The quotient space X/~ carries the discrete topology.

Русский

Факторпространство X/~ имеет дискретную топологию.

LaTeX

$$$ \\text{DiscreteTopology}(X/\\sim)$$$

Lean4

instance : DiscreteTopology S :=
  discreteTopology_iff_isOpen_singleton.2 <|
    S.proj_surjective.forall.2 fun x =>
      by
      rw [← S.proj_isQuotientMap.isOpen_preimage, fiber_eq]
      exact S.isOpen_setOf_rel _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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