isCompact_uIcc — Mathlib

English

An unordered closed interval uIcc a b is compact in a compactIcc space.

Русский

Неупорядоченный закрытый интервал uIcc a b компактен в компактном пространстве Icc.

LaTeX

$$IsCompact (uIcc a b)$$

Lean4

/-- An unordered closed interval is compact. -/
theorem isCompact_uIcc {α : Type*} [LinearOrder α] [TopologicalSpace α] [CompactIccSpace α] {a b : α} :
    IsCompact (uIcc a b) :=
  isCompact_Icc

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