normalClosure_eq_iInf — Mathlib

English

ConjugatesOfSet s is contained in normalClosure s.

Русский

Конъюгаты множества s содержатся в нормальном замыкании s.

LaTeX

$$$ \mathrm{conjugatesOfSet}(s) \subseteq \mathrm{normalClosure}(s) $$$

Lean4

theorem normalClosure_eq_iInf : normalClosure s = ⨅ (N : Subgroup G) (_ : Normal N) (_ : s ⊆ N), N :=
  le_antisymm (le_iInf fun _ => le_iInf fun _ => le_iInf normalClosure_le_normal)
    (iInf_le_of_le (normalClosure s) (iInf_le_of_le (by infer_instance) (iInf_le_of_le subset_normalClosure le_rfl)))

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