English
Given a neighborhood U of the identity, there exists a neighborhood V of the identity that is closed, symmetric, and V·V ⊆ U.
Русский
Для любого окрестности U тождения единицы существует окрестность V с замкнутостью, симметричностью и V·V ⊆ U.
LaTeX
$$$\\forall U \\in \\mathcal{N}(1),\\ exists\\ V \\in \\mathcal{N}(1),\\ IsClosed(V) \\wedge V^{-1} = V \\wedge V\\cdot V \\subseteq U$$$
Lean4
/-- Given a neighborhood `U` of the identity, one may find a neighborhood `V` of the identity which
is closed, symmetric, and satisfies `V * V ⊆ U`. -/
@[to_additive /-- Given a neighborhood `U` of the identity, one may find a neighborhood `V` of the
identity which is closed, symmetric, and satisfies `V + V ⊆ U`. -/
]
theorem exists_closed_nhds_one_inv_eq_mul_subset {U : Set G} (hU : U ∈ 𝓝 1) :
∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U :=
by
rcases exists_open_nhds_one_mul_subset hU with ⟨V, V_open, V_mem, hV⟩
rcases exists_mem_nhds_isClosed_subset (V_open.mem_nhds V_mem) with ⟨W, W_mem, W_closed, hW⟩
refine
⟨W ∩ W⁻¹, Filter.inter_mem W_mem (inv_mem_nhds_one G W_mem), W_closed.inter W_closed.inv, by simp [inter_comm], ?_⟩
calc
W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ W * W := mul_subset_mul inter_subset_left inter_subset_left
_ ⊆ V * V := (mul_subset_mul hW hW)
_ ⊆ U := hV
