English
Let M be a topological monoid with continuous multiplication. Then for every a in M, the product of the neighborhood filter at 1 with the neighborhood filter at a equals the neighborhood filter at a: nhds(1) · nhds(a) = nhds(a).
Русский
Пусть M — топологическая моноида с непрерывным умножением. Тогда для каждого a ∈ M выполняется 𝓝(1) · 𝓝(a) = 𝓝(a).
LaTeX
$$$\mathcal N(1) \cdot \mathcal N(a) = \mathcal N(a)$$$
Lean4
@[to_additive (attr := simp)]
theorem nhds_one_mul_nhds {M} [MulOneClass M] [TopologicalSpace M] [ContinuousMul M] (a : M) : 𝓝 (1 : M) * 𝓝 a = 𝓝 a :=
((le_nhds_mul _ _).trans_eq <| congr_arg _ (one_mul a)).antisymm <| le_mul_of_one_le_left' <| pure_le_nhds 1
