ι : Type ?u.43574
B : Type u_2
F : Type u_3
E : B → Type ?u.43585
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt (↑e.toLocalHomeomorph ∘ f) x

ι : Type ?u.43574
B : Type u_2
F : Type u_3
E : B → Type ?u.43585
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x
ι : Type ?u.43574
B : Type u_2
F : Type u_3
E : B → Type ?u.43585
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt f x
rw [e.continuousAt_iff_continuousAt_comp_left]
ι : Type ?u.43574
B : Type u_2
F : Type u_3
E : B → Type ?u.43585
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x
ι : Type ?u.43574
B : Type u_2
F : Type u_3
E : B → Type ?u.43585
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ f ⁻¹' e.source ∈ 𝓝 x
rw [e.source_eq, ← preimage_comp]
no goals
ι : Type ?u.43574
B : Type u_2
F : Type u_3
E : B → Type ?u.43585
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ proj ∘ f ⁻¹' e.baseSet ∈ 𝓝 x
exact hf_proj.preimage_mem_nhds (e.open_baseSet.mem_nhds he)
no goals
ι : Type ?u.43574
B : Type u_2
F : Type u_3
E : B → Type ?u.43585
Z : Type u_4
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
proj : Z → B
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace (TotalSpace E)
e✝ : Trivialization F proj
x✝ : Z
X : Type u_1
inst✝ : TopologicalSpace X
f : X → Z
x : X
e : Trivialization F proj
hf_proj : ContinuousAt (proj ∘ f) x
he : proj (f x) ∈ e.baseSet
hf : ContinuousAt (↑e ∘ f) x
⊢ ContinuousAt (↑e.toLocalHomeomorph ∘ f) x
exact hf