normalCore_isClosed — Mathlib

English

For a subgroup H of G, if H is closed then its normal core is closed as a subset of G.

Русский

Для подгруппы H внутри G, если H замкнута, то её нормальное ядро является замкнутым подмножеством G.

LaTeX

$$$ \\text{IsClosed}(H) \\Rightarrow \\text{IsClosed}(H\\_{\\text{normalCore}}) $$$

Lean4

theorem normalCore_isClosed (H : Subgroup G) (h : IsClosed (H : Set G)) : IsClosed (H.normalCore : Set G) :=
  by
  rw [normalCore_eq_iInf_conjAct]
  push_cast
  apply isClosed_iInter
  intro g
  convert IsClosed.preimage (IsTopologicalGroup.continuous_conj (ConjAct.ofConjAct g⁻¹)) h using 1
  exact Set.ext (fun t ↦ Set.mem_smul_set_iff_inv_smul_mem)

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