English
Let s be a subset of a topological monoid M with continuous multiplication. If s contains a neighborhood of 1, there exists an open neighborhood V of 1 such that for all v ∈ V and w ∈ V, v · w ∈ s.
Русский
Пусть s ⊆ M, где M — топологический моноид с непрерывным умножением. Если s содержит окрестность 1, найдётся открытая окрестность V единицы, такая что для любых v, w ∈ V выполняется v·w ∈ s.
LaTeX
$$$(nhds\,1)\ni s \Rightarrow \exists V\,(IsOpen\ V) \land 1\in V \land \forall v\in V, \forall w\in V, v w \in s$$$
Lean4
@[to_additive exists_nhds_zero_half]
theorem exists_nhds_one_split {s : Set M} (hs : s ∈ 𝓝 (1 : M)) : ∃ V ∈ 𝓝 (1 : M), ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s :=
let ⟨V, Vo, V1, hV⟩ := exists_open_nhds_one_split hs
⟨V, IsOpen.mem_nhds Vo V1, hV⟩
