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

• isCoherentWith : Topology.IsCoherentWith {K : Set X | T2Space ↑K ∧ IsCompact K}