English
In a topological group G, the neighbourhood filter of a product equals the product of neighbourhood filters: 𝓝(xy) = 𝓝(x) · 𝓝(y).
Русский
В топологической группе G окрестностная фильтрация под произведением равна произведению окрестностных фильтраций: 𝓝(xy) = 𝓝(x) · 𝓝(y).
LaTeX
$$$\nhds(xy) = \nhds(x) \cdot \nhds(y).$$$
Lean4
@[to_additive]
theorem nhds_mul (x y : G) : 𝓝 (x * y) = 𝓝 x * 𝓝 y :=
calc
𝓝 (x * y) = map (x * ·) (map (· * y) (𝓝 1 * 𝓝 1)) := by simp
_ = map₂ (fun a b => x * (a * b * y)) (𝓝 1) (𝓝 1) := by rw [← map₂_mul, map_map₂, map_map₂]
_ = map₂ (fun a b => x * a * (b * y)) (𝓝 1) (𝓝 1) := by simp only [mul_assoc]
_ = 𝓝 x * 𝓝 y := by
rw [← map_mul_left_nhds_one x, ← map_mul_right_nhds_one y, ← map₂_mul, map₂_map_left, map₂_map_right]
