ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.29164
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.fst ∈ baseSet Z i ∩ baseSet Z j ∧ p.snd ∈ univ ↔ p.fst ∈ baseSet Z i ∩ baseSet Z j
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.29164
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p ∈ (trivChange Z i j).toLocalEquiv.source ↔ p.fst ∈ baseSet Z i ∩ baseSet Z j
erw [mem_prod]
no goals
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.29164
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
p : B × F
⊢ p.fst ∈ baseSet Z i ∩ baseSet Z j ∧ p.snd ∈ univ ↔ p.fst ∈ baseSet Z i ∩ baseSet Z j
simp