mk'' — Mathlib

English

If for all a < b the open interval (a,b) is compact, then α is CompactIccSpace.

Русский

Если для всех a < b открытый интервал (a,b) компактен, то α—CompactIccSpace.

LaTeX

$$(∀ {a b}, a < b → IsCompact (Icc a b)) → CompactIccSpace α$$

Lean4

theorem mk'' [TopologicalSpace α] [PartialOrder α] (h : ∀ {a b : α}, a < b → IsCompact (Icc a b)) : CompactIccSpace α :=
  .mk' fun hab => hab.eq_or_lt.elim (by rintro rfl; simp) h

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