instNonemptyQuotient

Mathlib.Topology.DiscreteQuotient

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

English

If X is nonempty, then the quotient X/~ is nonempty.

Русский

Если X непусто, то факторпространство X/~ непусто.

LaTeX

$$$ X \\neq \\varnothing \\Rightarrow X/\\sim \\neq \\varnothing $$$

Lean4

instance [Nonempty X] : Nonempty S :=
  Nonempty.map S.proj ‹_›

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

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

Разделы

Аффилиация

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