comap — Mathlib

English

Under a bijection f: G ≃* N, the normal closure commutes with comap: normalClosure(f^{-1}(s)) = (normalClosure s).comap f.

Русский

При биекции f: G ≃* N нормальное замыкание commute с предобразом: normalClosure(f^{-1}(s)) = (normalClosure s).comap f.

LaTeX

$$$ \\operatorname{normalClosure}(f^{-1}(s)) = (\\operatorname{normalClosure}(s)).comap f $$$

Lean4

@[to_additive]
theorem comap {H : Subgroup N} (hH : H.Normal) (f : G →* N) : (H.comap f).Normal :=
  ⟨fun _ => by simp +contextual [Subgroup.mem_comap, hH.conj_mem]⟩

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