compactSpace_of_completeLinearOrder

English

A complete linear order is a compact space.

Русский

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

LaTeX

$$CompactSpace α$$

Lean4

/-- A complete linear order is a compact space.

We do not register an instance for a `[CompactIccSpace α]` because this would only add instances
for products (indexed or not) of complete linear orders, and we have instances with higher priority
that cover these cases. -/
instance (priority := 100) compactSpace_of_completeLinearOrder {α : Type*} [CompleteLinearOrder α] [TopologicalSpace α]
    [OrderTopology α] : CompactSpace α :=
  ⟨by simp only [← Icc_bot_top, isCompact_Icc]⟩

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