ι : Type ?u.61867
B : Type u_2
F : Type u_3
X : Type ?u.61876
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
x : E b
⊢ b ∈ (pretrivializationAt a b).baseSet
ι : Type ?u.61867
B : Type u_2
F : Type u_3
X : Type ?u.61876
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
x : E b
⊢ totalSpaceMk b x ∈ (pretrivializationAt a b).source
simp only [(a.pretrivializationAt b).source_eq, mem_preimage, TotalSpace.proj]
no goals
ι : Type ?u.61867
B : Type u_2
F : Type u_3
X : Type ?u.61876
inst✝³ : TopologicalSpace X
E : B → Type u_1
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
b : B
x : E b
⊢ b ∈ (pretrivializationAt a b).baseSet
exact a.mem_base_pretrivializationAt b