isTerminalPUnit

Mathlib.Topology.Category.CompHausLike.Limits

URI: https://scilib.ai/kg/mathlib#CompHausLike.isTerminalPUnit

Lean4

/-- A one-element space is terminal in `CompHaus` -/
def isTerminalPUnit [HasProp P PUnit.{u + 1}] : IsTerminal (CompHausLike.of P PUnit.{u + 1}) :=
  haveI : ∀ X, Unique (X ⟶ CompHausLike.of P PUnit.{u + 1}) := fun _ ↦
    ⟨⟨ofHom _ ⟨fun _ ↦ PUnit.unit, continuous_const⟩⟩, fun _ ↦ rfl⟩
  Limits.IsTerminal.ofUnique _

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

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

Разделы

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

Аффилиация

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