mk' — Mathlib

English

If every Icc interval in α is compact, then α carries a CompactIccSpace structure.

Русский

Если каждая область Icc в α компактна, то α имеет структуру CompactIccSpace.

LaTeX

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

Lean4

theorem mk' [TopologicalSpace α] [Preorder α] (h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)) : CompactIccSpace α where
  isCompact_Icc {a b} := by_cases h fun hab => by rw [Icc_eq_empty hab]; exact isCompact_empty

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