𝕜 : Type u_4
E : Type u_1
M : Type u_2
H : Type u_3
E' : Type ?u.149123
M' : Type ?u.149126
H' : Type ?u.149129
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s✝ t : Set M
s : Set E
hs : IsOpen s
⊢ IsOpen ((extend f I).source ∩ ↑(extend f I) ⁻¹' s)
𝕜 : Type u_4
E : Type u_1
M : Type u_2
H : Type u_3
E' : Type ?u.149123
M' : Type ?u.149126
H' : Type ?u.149129
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s✝ t : Set M
s : Set E
hs : IsOpen s
⊢ IsOpen (f.source ∩ ↑(extend f I) ⁻¹' s)
rw [← extend_source f I]
no goals
𝕜 : Type u_4
E : Type u_1
M : Type u_2
H : Type u_3
E' : Type ?u.149123
M' : Type ?u.149126
H' : Type ?u.149129
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s✝ t : Set M
s : Set E
hs : IsOpen s
⊢ IsOpen ((extend f I).source ∩ ↑(extend f I) ⁻¹' s)
exact isOpen_extend_preimage' f I hs