English
An open neighborhood U of the identity in G × G contains the square of an open subgroup V.
Русский
Окрестность единицы в G × G содержит квадрат некоторой открытой подгруппы V.
LaTeX
$$∃ V : OpenSubgroup G, (V : Set G) ×ˢ (V : Set G) ⊆ U$$
Lean4
/-- An open neighborhood of the identity in the Cartesian square of a nonarchimedean group
contains the Cartesian square of an open neighborhood in the group. -/
@[to_additive NonarchimedeanAddGroup.prod_self_subset /-- An open neighborhood of the identity in
the Cartesian square of a nonarchimedean group contains the Cartesian square of
an open neighborhood in the group. -/
]
theorem prod_self_subset {U} (hU : U ∈ 𝓝 (1 : G × G)) : ∃ V : OpenSubgroup G, (V : Set G) ×ˢ (V : Set G) ⊆ U :=
let ⟨V, W, h⟩ := prod_subset hU
⟨V ⊓ W, by refine Set.Subset.trans (Set.prod_mono ?_ ?_) ‹_› <;> simp⟩
