X : Type u_1
Y : Type ?u.48324
Z : Type ?u.48327
α : Type ?u.48330
ι : Type ?u.48333
π : ι → Type ?u.48338
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)
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) ⊆ s
X : Type u_1
Y : Type ?u.48324
Z : Type ?u.48327
α : Type ?u.48330
ι : Type ?u.48333
π : ι → Type ?u.48338
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)
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) = s
refine' Subset.antisymm _ (subset_preimage_image _ _)
case intro.intro
X : Type u_1
Y : Type ?u.48324
Z : Type ?u.48327
α : Type ?u.48330
ι : Type ?u.48333
π : ι → Type ?u.48338
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)
hs : IsOpen s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s
X : Type u_1
Y : Type ?u.48324
Z : Type ?u.48327
α : Type ?u.48330
ι : Type ?u.48333
π : ι → Type ?u.48338
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)
hs : IsOpen s
⊢ mk ⁻¹' (mk '' s) ⊆ s
rintro x ⟨y, hys, hxy⟩
no goals
case intro.intro
X : Type u_1
Y : Type ?u.48324
Z : Type ?u.48327
α : Type ?u.48330
ι : Type ?u.48333
π : ι → Type ?u.48338
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)
hs : IsOpen s
x y : X
hys : y ∈ s
hxy : mk y = mk x
⊢ x ∈ s
exact ((mk_eq_mk.1 hxy).mem_open_iff hs).1 hys