map_stabilizer_le — Mathlib

English

The image of a stabilizer under a group homomorphism maps into the stabilizer of the image of the set.

Русский

Образ стабилизатора под гомоморфизмом отображается в стабилизатор образа множества.

LaTeX

$$$ (\operatorname{Stab}_G(s))^f \le \operatorname{Stab}_H(f(s)) $$$

Lean4

@[to_additive]
theorem map_stabilizer_le (f : G →* H) (s : Set G) : (stabilizer G s).map f ≤ stabilizer H (f '' s) :=
  by
  rintro a
  simp only [Subgroup.mem_map, mem_stabilizer_iff, forall_exists_index, and_imp]
  rintro a ha rfl
  rw [← image_smul_distrib, ha]

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