class PiBase.HasGδDiagonal (X : Type u_1) [TopologicalSpace X] : Prop

• has_g_delta_diagonal : IsGδ (Set.diagonal X)