ι : Type ?u.8420
α : Type ?u.8423
X : Type ?u.8426
M : Type u_1
N : Type ?u.8432
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x x_1 => x * x_1) (𝓝 (a, b)) ≤ 𝓝 (a * b)
ι : Type ?u.8420
α : Type ?u.8423
X : Type ?u.8426
M : Type u_1
N : Type ?u.8432
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ 𝓝 a * 𝓝 b ≤ 𝓝 (a * b)
rw [← map₂_mul, ← map_uncurry_prod, ← nhds_prod_eq]
no goals
ι : Type ?u.8420
α : Type ?u.8423
X : Type ?u.8426
M : Type u_1
N : Type ?u.8432
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : Mul M
inst✝ : ContinuousMul M
a b : M
⊢ map (Function.uncurry fun x x_1 => x * x_1) (𝓝 (a, b)) ≤ 𝓝 (a * b)
exact continuous_mul.tendsto _