English
Given a neighborhood U of 1 in a topological monoid M with continuous multiplication, there exists an open neighborhood V of 1 such that V · V ⊆ U.
Русский
Для любой окрестности U точки 1 в топологическом моноиде M с непрерывным умножением существует открытая окрестность V точки 1 такая, что V · V ⊆ U.
LaTeX
$$$\exists V\; IsOpen V \land 1\in V \land V\cdot V \subseteq U$$$
Lean4
/-- Given a neighborhood `U` of `1` there is an open neighborhood `V` of `1`
such that `V * V ⊆ U`. -/
@[to_additive /-- Given an open neighborhood `U` of `0` there is an open neighborhood `V` of `0`
such that `V + V ⊆ U`. -/
]
theorem exists_open_nhds_one_mul_subset {U : Set M} (hU : U ∈ 𝓝 (1 : M)) :
∃ V : Set M, IsOpen V ∧ (1 : M) ∈ V ∧ V * V ⊆ U := by
simpa only [mul_subset_iff] using exists_open_nhds_one_split hU
