normal_iInf_normal — Mathlib

English

If each a_i is normal in G, then the meet over i of a_i is normal in G.

Русский

Если каждая a_i нормальна в G, то их пересечение нормальна в G.

LaTeX

$$∀ i, (a_i).Normal → (iInf a).Normal$$

Lean4

@[to_additive]
theorem normal_iInf_normal {ι : Sort*} {a : ι → Subgroup G} (norm : ∀ i : ι, (a i).Normal) : (iInf a).Normal :=
  by
  constructor
  intro g g_in_iInf h
  rw [Subgroup.mem_iInf] at g_in_iInf ⊢
  intro i
  exact (norm i).conj_mem g (g_in_iInf i) h

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