theorem t2Space_iff_of_continuous_surjective_open {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [TopologicalSpace β] {π : α → β} (hcont : Continuous π) (hsurj : Function.Surjective π) (hop : IsOpenMap π) : T2Space β ↔ IsClosed {q : α × α | π q.1 = π q.2}