le_normalizer_comap — Mathlib

English

For a homomorphism f: N → G, the preimage of the normalizer of H under f is contained in the normalizer of the preimage of H.

Русский

Для гомоморфизма f: N → G прообраз нормализатора H по f содержится в нормализаторе прообраза H.

LaTeX

$$$H.\operatorname{normalizer}.\operatorname{comap}(f) \le (H.\operatorname{comap}(f)).\operatorname{normalizer}$$$

Lean4

/-- The preimage of the normalizer is contained in the normalizer of the preimage. -/
@[to_additive /-- The preimage of the normalizer is contained in the normalizer of the preimage. -/
    ]
theorem le_normalizer_comap (f : N →* G) : H.normalizer.comap f ≤ (H.comap f).normalizer := fun x =>
  by
  simp only [mem_normalizer_iff, mem_comap]
  intro h n
  simp [h (f n)]

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