α : Type u
β : Type v
γ : Type ?u.35295
δ : Type ?u.35298
ε : Type ?u.35301
ζ : Type ?u.35304
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
ιa : Type u_1
ιb : Type u_2
pa : ιa → Prop
pb : ιb → Prop
sa : ιa → Set α
sb : ιb → Set β
a : α
b : β
ha : HasBasis (𝓝 a) pa sa
hb : HasBasis (𝓝 b) pb sb
⊢ HasBasis (𝓝 a ×ˢ 𝓝 b) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
α : Type u
β : Type v
γ : Type ?u.35295
δ : Type ?u.35298
ε : Type ?u.35301
ζ : Type ?u.35304
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
ιa : Type u_1
ιb : Type u_2
pa : ιa → Prop
pb : ιb → Prop
sa : ιa → Set α
sb : ιb → Set β
a : α
b : β
ha : HasBasis (𝓝 a) pa sa
hb : HasBasis (𝓝 b) pb sb
⊢ HasBasis (𝓝 (a, b)) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
rw [nhds_prod_eq]
no goals
α : Type u
β : Type v
γ : Type ?u.35295
δ : Type ?u.35298
ε : Type ?u.35301
ζ : Type ?u.35304
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
ιa : Type u_1
ιb : Type u_2
pa : ιa → Prop
pb : ιb → Prop
sa : ιa → Set α
sb : ιb → Set β
a : α
b : β
ha : HasBasis (𝓝 a) pa sa
hb : HasBasis (𝓝 b) pb sb
⊢ HasBasis (𝓝 a ×ˢ 𝓝 b) (fun i => pa i.fst ∧ pb i.snd) fun i => sa i.fst ×ˢ sb i.snd
exact ha.prod hb