instInhabitedCtopSet

Mathlib.Data.Analysis.Topology

URI: https://scilib.ai/kg/mathlib#instInhabitedCtopSet

Lean4

instance : Inhabited (Ctop α (Set α)) :=
  ⟨{  f := id
      top := singleton
      top_mem := mem_singleton
      inter := fun s t _ _ ↦ s ∩ t
      inter_mem := fun _s _t _a ↦ id
      inter_sub := fun _s _t _a _ha ↦ Subset.rfl }⟩

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

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

Разделы

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

Аффилиация

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