instInhabited

Mathlib.Topology.Sets.Compacts

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.NonemptyCompacts.instInhabited

Lean4

/-- In an inhabited space, the type of nonempty compact subsets is also inhabited, with
default element the singleton set containing the default element. -/
instance [Inhabited α] : Inhabited (NonemptyCompacts α) :=
  ⟨{  carrier := { default }
      isCompact' := isCompact_singleton
      nonempty' := singleton_nonempty _ }⟩

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

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

Разделы

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

Аффилиация

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