ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32284
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p.fst ∈ baseSet Z i ∧ p.snd ∈ univ ↔ p.fst ∈ baseSet Z i
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32284
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p ∈ (localTrivAsLocalEquiv Z i).target ↔ p.fst ∈ baseSet Z i
erw [mem_prod]
no goals
ι : Type u_3
B : Type u_1
F : Type u_2
X : Type ?u.32284
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : B × F
⊢ p.fst ∈ baseSet Z i ∧ p.snd ∈ univ ↔ p.fst ∈ baseSet Z i
simp only [and_true_iff, mem_univ]