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

• closed_continuous ⦃K : Type u⦄ {x✝ : TopologicalSpace K} (f : K → X × X) : T2Space K → CompactSpace K → Continuous f → IsClosed (f ⁻¹' Set.diagonal X)