class PiBase.StronglyZeroDimensionalSpace (X : Type u_1) [TopologicalSpace X] : Prop

• disjoint_clopen {s t : Set X} (hs : IsZero s) (ht : IsZero t) (st : s ∩ t = ∅) : ∃ (s' : Set X) (t' : Set X), IsClopen s' ∧ IsClopen t' ∧ s ⊆ s' ∧ t ⊆ t' ∧ s' ∩ t' = ∅