English
An open neighborhood of the identity in G × K contains a product V × W of open subgroups from each factor.
Русский
Окрестность единицы в G × K содержит произведение базовых открытых подгрупп V × W.
LaTeX
$$∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (V : Set G) ×ˢ (W : Set K) ⊆ U$$
Lean4
/-- An open neighborhood of the identity in the Cartesian product of two nonarchimedean groups
contains the Cartesian product of an open neighborhood in each group. -/
@[to_additive NonarchimedeanAddGroup.prod_subset /-- An open neighborhood of the identity in
the Cartesian product of two nonarchimedean groups contains the Cartesian product of
an open neighborhood in each group. -/
]
theorem prod_subset {U} (hU : U ∈ 𝓝 (1 : G × K)) :
∃ (V : OpenSubgroup G) (W : OpenSubgroup K), (V : Set G) ×ˢ (W : Set K) ⊆ U :=
by
rw [nhds_prod_eq, Filter.mem_prod_iff] at hU
rcases hU with ⟨U₁, hU₁, U₂, hU₂, h⟩
obtain ⟨V, hV⟩ := is_nonarchimedean _ hU₁
obtain ⟨W, hW⟩ := is_nonarchimedean _ hU₂
use V
grind
