case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.329305
δ : Type ?u.329308
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (f '' (t ∩ s))

case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.329305
δ : Type ?u.329308
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
α : Type u_1
β : Type u_2
γ : Type ?u.329305
δ : Type ?u.329308
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
⊢ ContinuousOn finv (f '' s)
refine' continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), _, _⟩
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.329305
δ : Type ?u.329308
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (Set.restrict s f '' (Subtype.val ⁻¹' t))
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.329305
δ : Type ?u.329308
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (f '' (t ∩ s))
rw [← image_restrict]
no goals
case refine'_1
α : Type u_1
β : Type u_2
γ : Type ?u.329305
δ : Type ?u.329308
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ IsOpen (Set.restrict s f '' (Subtype.val ⁻¹' t))
exact h _ (ht.preimage continuous_subtype_val)
no goals
case refine'_2
α : Type u_1
β : Type u_2
γ : Type ?u.329305
δ : Type ?u.329308
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : IsOpenMap (Set.restrict s f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen t
⊢ finv ⁻¹' t ∩ f '' s = f '' (t ∩ s) ∩ f '' s
rw [inter_eq_self_of_subset_left (image_subset f (inter_subset_right t s)), hleft.image_inter']