ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.46750
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
⊢ { fst := b, snd := a }.fst ∈ (localTriv Z (indexAt Z b)).baseSet
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.46750
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
⊢ { fst := b, snd := a } ∈ (localTrivAt Z b).toLocalHomeomorph.toLocalEquiv.source
rw [localTrivAt, mem_localTriv_source]
no goals
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.46750
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
b : B
a : F
⊢ { fst := b, snd := a }.fst ∈ (localTriv Z (indexAt Z b)).baseSet
exact Z.mem_baseSet_at b