no goals
α : Type ?u.22242
X : Type u_1
Y : Type ?u.22248
Z : Type ?u.22251
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
S : DiscreteQuotient X
inst✝ : DiscreteTopology X
x y : X
⊢ proj ⊥ x = proj ⊥ y ↔ x = y
simp