ι : Type ?u.56599
B : Type u_1
F : Type u_2
X : Type ?u.56608
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
z : B × F
H : z ∈ e.target
U : Set (TotalSpace E)
h : U ∈ 𝓝 (↑(LocalEquiv.symm e.toLocalEquiv) z)
⊢ coinduced (fun x => ↑(LocalEquiv.symm e.toLocalEquiv) ↑x) inferInstance ≤ totalSpaceTopology a
ι : Type ?u.56599
B : Type u_1
F : Type u_2
X : Type ?u.56608
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
⊢ ContinuousOn (↑(LocalEquiv.symm e.toLocalEquiv)) e.target
refine' fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono _) U h)
no goals
ι : Type ?u.56599
B : Type u_1
F : Type u_2
X : Type ?u.56608
inst✝³ : TopologicalSpace X
E : B → Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
z : B × F
H : z ∈ e.target
U : Set (TotalSpace E)
h : U ∈ 𝓝 (↑(LocalEquiv.symm e.toLocalEquiv) z)
⊢ coinduced (fun x => ↑(LocalEquiv.symm e.toLocalEquiv) ↑x) inferInstance ≤ totalSpaceTopology a
exact le_iSup₂ (α := TopologicalSpace (TotalSpace E)) e he