inhabitedQuotient

Mathlib.Topology.DiscreteQuotient

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

Lean4

instance inhabitedQuotient [Inhabited X] : Inhabited S :=
  ⟨S.proj default⟩
    -- TODO: add instances about `Nonempty (Quot _)`/`Nonempty (Quotient _)`

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

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

Разделы

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

Аффилиация

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