pointwise ops on nhds

Stream: Is there code for X?

[Adam Topaz]

Does anyone know of an efficient way to prove lemmas of the following form?

import order.filter.pointwise
import topology.algebra.ring

open_locale pointwise topological_space

example {G : Type*} [topological_space G] [group G] [topological_group G]
  (x y : G) : 𝓝 x * 𝓝 y ≤ 𝓝 (x * y) :=
sorry

[Adam Topaz]

ping @Jack McKoen

[Yaël Dillies]

Look for a lemma about docs#filter.map₂

[Yaël Dillies]

If it desn't exist, look for the set or finset version

[Anatole Dedecker]

import order.filter.pointwise
import topology.algebra.ring

open filter
open_locale pointwise topological_space

example {G : Type*} [topological_space G] [group G] [topological_group G]
  (x y : G) : 𝓝 x * 𝓝 y ≤ 𝓝 (x * y) :=
begin
  rw [← map₂_mul, ← map_prod_eq_map₂, ← nhds_prod_eq],
  exact continuous_mul.tendsto (x, y)
end

[Adam Topaz]

Nice! Thanks!