α : Type ?u.6073
X : Type u_1
Y : Type ?u.6079
Z : Type ?u.6082
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsClopen (proj S ⁻¹' {proj S x})
α : Type ?u.6073
X : Type u_1
Y : Type ?u.6079
Z : Type ?u.6082
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsClopen (setOf (Setoid.Rel S.toSetoid x))
rw [← fiber_eq]
no goals
α : Type ?u.6073
X : Type u_1
Y : Type ?u.6079
Z : Type ?u.6082
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
S : DiscreteQuotient X
x : X
⊢ IsClopen (proj S ⁻¹' {proj S x})
apply isClopen_preimage