English
Let s be a subset of a topological monoid M with continuous multiplication. If s contains a neighborhood of 1, then there exists an open neighborhood V of 1 such that for all v, w ∈ V we have v · w ∈ s.
Русский
Пусть s ⊆ M, где M — топологический моноид с непрерывным умножением. Если s содержит окрестность 1, то существует открытая окрестность V единицы such that для всех v, w ∈ V выполняется v·w ∈ s.
LaTeX
$$$(\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_open_nhds_zero_half]
theorem exists_open_nhds_one_split {s : Set M} (hs : s ∈ 𝓝 (1 : M)) :
∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s :=
by
have : (fun a : M × M => a.1 * a.2) ⁻¹' s ∈ 𝓝 ((1, 1) : M × M) := tendsto_mul (by simpa only [one_mul] using hs)
simpa only [prod_subset_iff] using exists_nhds_square this
