α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.96477
ζ : Type ?u.96480
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (a : α × γ), 𝓝 (f a.fst, g a.snd) ≤ map (fun p => (f p.fst, g p.snd)) (𝓝 a)
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.96477
ζ : Type ?u.96480
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap fun p => (f p.fst, g p.snd)
rw [isOpenMap_iff_nhds_le]
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.96477
ζ : Type ?u.96480
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
a : α
b : γ
⊢ 𝓝 (f (a, b).fst, g (a, b).snd) ≤ map (fun p => (f p.fst, g p.snd)) (𝓝 (a, b))
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.96477
ζ : Type ?u.96480
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (a : α × γ), 𝓝 (f a.fst, g a.snd) ≤ map (fun p => (f p.fst, g p.snd)) (𝓝 a)
rintro ⟨a, b⟩
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.96477
ζ : Type ?u.96480
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
a : α
b : γ
⊢ 𝓝 (f (a, b).fst) ×ˢ 𝓝 (g (a, b).snd) ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.96477
ζ : Type ?u.96480
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
a : α
b : γ
⊢ 𝓝 (f (a, b).fst, g (a, b).snd) ≤ map (fun p => (f p.fst, g p.snd)) (𝓝 (a, b))
rw [nhds_prod_eq, nhds_prod_eq, ← Filter.prod_map_map_eq]
no goals
case mk
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.96477
ζ : Type ?u.96480
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : IsOpenMap f
hg : IsOpenMap g
a : α
b : γ
⊢ 𝓝 (f (a, b).fst) ×ˢ 𝓝 (g (a, b).snd) ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)
exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)