case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.343466
δ : Type ?u.343469
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ f ⁻¹' t = s ∩ f ⁻¹' t
α : Type u_1
β : Type u_2
γ : Type ?u.343466
δ : Type ?u.343469
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ IsOpen (f ⁻¹' t)
convert (continuousOn_open_iff hs).mp h t ht
no goals
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type ?u.343466
δ : Type ?u.343469
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen s
hp : f ⁻¹' t ⊆ s
ht : IsOpen t
⊢ f ⁻¹' t = s ∩ f ⁻¹' t
rw [inter_comm, inter_eq_self_of_subset_left hp]