English
Let G be a topological group. The map g ↦ 𝓝(g), sending each element to its neighborhood filter, is multiplicative: for all g,h ∈ G, 𝓝(gh) = 𝓝(g) · 𝓝(h). Equivalently, the assignment g ↦ 𝓝(g) is a multiplicative homomorphism from G to the semigroup of filters on G.
Русский
Пусть G — топологическая группа. Отображение g ↦ 𝓝(g), отправляющее элемент в его фильтр окрестностей, сохраняет умножение: для любых g,h ∈ G выполняется 𝓝(gh) = 𝓝(g) · 𝓝(h). Иначе говоря, отображение g ↦ 𝓝(g) образует мультипликативную гомоморфизмную структуру между G и фильтрами на G.
LaTeX
$$$ \\forall g,h \\in G:\\; \\mathcal{N}(gh) = \\mathcal{N}(g) \\ast \\mathcal{N}(h) \\qquad\\; \\text{(nhds is a MulHom)} $$$
Lean4
/-- On a topological group, `𝓝 : G → Filter G` can be promoted to a `MulHom`. -/
@[to_additive (attr := simps) /--
On an additive topological group, `𝓝 : G → Filter G` can be promoted to an `AddHom`. -/
]
def nhdsMulHom : G →ₙ* Filter G where
toFun := 𝓝
map_mul' _ _ := nhds_mul _ _
