English
There exists an open subgroup contained in a given clopen neighborhood near the identity within a compact topological group.
Русский
Существует открытая подгруппа, содержащаяся в заданном клипойнном окрестном множестве около единицы внутри компактной топологической группы.
LaTeX
$$$\\exists H: OpenSubgroup G, H \\subseteq W$$$
Lean4
@[to_additive]
theorem exist_openSubgroup_sub_clopen_nhds_of_one {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[CompactSpace G] {W : Set G} (WClopen : IsClopen W) (einW : 1 ∈ W) : ∃ H : OpenSubgroup G, (H : Set G) ⊆ W :=
by
rcases exists_mulInvClosureNhd WClopen with ⟨V, hV⟩
let S : Subgroup G :=
{ carrier := ⋃ n, V ^ (n + 1)
mul_mem' := fun ha hb ↦ by
rcases mem_iUnion.mp ha with ⟨k, hk⟩
rcases mem_iUnion.mp hb with ⟨l, hl⟩
apply mem_iUnion.mpr
use k + 1 + l
rw [add_assoc, pow_add]
exact Set.mul_mem_mul hk hl
one_mem' := by
apply mem_iUnion.mpr
use 0
simp [mem_of_mem_nhds hV.nhds]
inv_mem' := fun ha ↦ by
rcases mem_iUnion.mp ha with ⟨k, hk⟩
apply mem_iUnion.mpr
use k
rw [← hV.inv]
simpa only [inv_pow, Set.mem_inv, inv_inv] using hk }
have : IsOpen (⋃ n, V ^ (n + 1)) := by
refine isOpen_iUnion (fun n ↦ ?_)
rw [pow_succ]
exact hV.isOpen.mul_left
use ⟨S, this⟩
have mulVpow (n : ℕ) : W * V ^ (n + 1) ⊆ W := by
induction n with
| zero => simp [hV.mul]
| succ n ih =>
rw [pow_succ, ← mul_assoc]
exact (Set.mul_subset_mul_right ih).trans hV.mul
have (n : ℕ) : V ^ (n + 1) ⊆ W * V ^ (n + 1) := by
intro x xin
rw [Set.mem_mul]
use 1, einW, x, xin
rw [one_mul]
apply iUnion_subset fun i _ a ↦ mulVpow i (this i a)
