comap_normalizer_eq_of_le_range — Mathlib

English

If H ≤ f.range, then comap f H.normalizer = (comap f H).normalizer.

Русский

Если H ≤ f.range, то comap f H.normalizer = (comap f H).normalizer.

LaTeX

$$$H \le f.\mathrm{range} \Rightarrow \mathrm{comap}(f)\, H.\mathrm{normalizer} = (\mathrm{comap}(f)H).\mathrm{normalizer}$$$

Lean4

@[to_additive]
theorem comap_normalizer_eq_of_le_range {f : N →* G} (h : H ≤ f.range) :
    comap f H.normalizer = (comap f H).normalizer :=
  by
  apply le_antisymm (le_normalizer_comap f)
  rw [← map_le_iff_le_comap]
  apply (le_normalizer_map f).trans
  rw [map_comap_eq_self h]

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