exists_mulInvClosureNhd — Mathlib

English

For a clopen W in a compact group, there exists an open subgroup H contained in W.

Русский

Для клипойнного W в компактной группе существует открытая подгруппа H, содержащаяся в W.

LaTeX

$$$\\exists H\\ (H : OpenSubgroup G) \\text{ such that } (H : Set G) \\subseteq W$$$

Lean4

@[to_additive]
theorem exists_mulInvClosureNhd {W : Set G} (WClopen : IsClopen W) : ∃ T, mulInvClosureNhd T W :=
  by
  rcases exist_mul_closure_nhds WClopen with ⟨S, Smemnhds, mulclose⟩
  rcases mem_nhds_iff.mp Smemnhds with ⟨U, UsubS, Uopen, onememU⟩
  use U ∩ U⁻¹
  constructor
  · simp [Uopen.mem_nhds onememU, inv_mem_nhds_one]
  · simp [inter_comm]
  · exact Uopen.inter Uopen.inv
  · exact fun a ha ↦ mulclose (mul_subset_mul_left UsubS (mul_subset_mul_left inter_subset_left ha))

Похожие утверждения