instInhabitedRealizerEmptyCollectionSet

Mathlib.Data.Analysis.Topology

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

Lean4

instance [TopologicalSpace α] : Inhabited (Compact.Realizer (∅ : Set α)) :=
  ⟨fun {f} F x h hF ↦ by
    suffices f = ⊥ from absurd this h
    rw [← F.eq, eq_bot_iff]
    exact fun s _ ↦ ⟨x, hF.trans s.empty_subset⟩⟩

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

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

Разделы

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

Аффилиация

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