English
For a clopen subset W of a compact topological group, there exists a neighborhood T of the identity such that W · T ⊆ W.
Русский
Для клипойнной (clopen) подмножества W в компактной топологической группе существует окрестность T единицы так, что W·T ⊆ W.
LaTeX
$$$\\exists T \\in 𝓝(1),\\ W \\cdot T \\subseteq W$$$
Lean4
@[to_additive]
theorem exist_mul_closure_nhds {W : Set G} (WClopen : IsClopen W) : ∃ T ∈ 𝓝 (1 : G), W * T ⊆ W :=
by
apply
WClopen.isClosed.isCompact.induction_on (p := fun S ↦ ∃ T ∈ 𝓝 (1 : G), S * T ⊆ W)
⟨Set.univ, by simp only [univ_mem, empty_mul, empty_subset, and_self]⟩
(fun _ _ huv ⟨T, hT, mem⟩ ↦ ⟨T, hT, (mul_subset_mul_right huv).trans mem⟩)
fun U V ⟨T₁, hT₁, mem1⟩ ⟨T₂, hT₂, mem2⟩ ↦
⟨T₁ ∩ T₂, inter_mem hT₁ hT₂, by
rw [union_mul]
exact
union_subset (mul_subset_mul_left inter_subset_left |>.trans mem1)
(mul_subset_mul_left inter_subset_right |>.trans mem2)⟩
intro x memW
have : (x, 1) ∈ (fun p ↦ p.1 * p.2) ⁻¹' W := by simp [memW]
rcases isOpen_prod_iff.mp (continuous_mul.isOpen_preimage W <| WClopen.2) x 1 this with
⟨U, V, Uopen, Vopen, xmemU, onememV, prodsub⟩
have h6 : U * V ⊆ W := mul_subset_iff.mpr (fun _ hx _ hy ↦ prodsub (mk_mem_prod hx hy))
exact
⟨U ∩ W, ⟨U, Uopen.mem_nhds xmemU, W, fun _ a ↦ a, rfl⟩, V, IsOpen.mem_nhds Vopen onememV, fun _ a ↦
h6 ((mul_subset_mul_right inter_subset_left) a)⟩
