class PiBase.HemicompactSpace (X : Type u) [TopologicalSpace X] : Prop

• hemicompact : ∃ (ι : Type u) (K : ι → Set X), Countable ι ∧ (∀ (i : ι), IsCompact (K i)) ∧ ⋃ (i : ι), K i = Set.univ ∧ ∀ (t : Set X), IsCompact t → ∃ (i : ι), t ⊆ K i