X : Type u_1
Y : Type ?u.58987
Z : Type ?u.58990
α : Type ?u.58993
ι : Type ?u.58996
π : ι → Type ?u.59001
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ IsClosed univ
X : Type u_1
Y : Type ?u.58987
Z : Type ?u.58990
α : Type ?u.58993
ι : Type ?u.58996
π : ι → Type ?u.59001
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ IsClosed (Set.range mk)
rw [range_mk]
no goals
X : Type u_1
Y : Type ?u.58987
Z : Type ?u.58990
α : Type ?u.58993
ι : Type ?u.58996
π : ι → Type ?u.59001
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x y z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
⊢ IsClosed univ
exact isClosed_univ