normalCore_eq_iSup — Mathlib

English

normalCore(H) equals the supremum over all normal subgroups containing H.

Русский

normalCore(H) равен наибольшему элементу над всеми нормальными подгруппами, содержащими H.

LaTeX

$$$ \mathrm{normalCore}(H) = \bigwedge_{N \trianglelefteq G,\ N \le H} N $$$

Lean4

theorem normalCore_eq_iSup (H : Subgroup G) : H.normalCore = ⨆ (N : Subgroup G) (_ : Normal N) (_ : N ≤ H), N :=
  le_antisymm (le_iSup_of_le H.normalCore (le_iSup_of_le H.normalCore_normal (le_iSup_of_le H.normalCore_le le_rfl)))
    (iSup_le fun _ => iSup_le fun _ => iSup_le normal_le_normalCore.mpr)

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