instSubsingletonQuotientTop

Mathlib.Topology.DiscreteQuotient

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

← MathLib Explorer

English

The quotient by the top relation is a singleton.

Русский

Факторпространство по топ-отношению образует один элемент.

LaTeX

$$$ X/\\top \\text{ is a singleton}$$$

Lean4

/-- The quotient by `⊤ : DiscreteQuotient X` is a `Subsingleton`. -/
instance : Subsingleton (⊤ : DiscreteQuotient X) where allEq := by rintro ⟨_⟩ ⟨_⟩; exact Quotient.sound trivial

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

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

Разделы

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

Аффилиация

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