set_mul_normalizer_comm — Mathlib

English

If S is contained in the normalizer of N, then S and N commute as sets: S N = N S.

Русский

Если S ⊆ N.normalizer, то множества S и N равны как множества: S N = N S.

LaTeX

$$$S\\cdot N = N\\cdot S \\quad\\text{whenever } S \\subseteq N\\text{.normalizer}$$$

Lean4

@[to_additive]
theorem set_mul_normalizer_comm (S : Set G) (N : Subgroup G) (hLE : S ⊆ N.normalizer) : S * N = N * S :=
  by
  rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]
  simp only [image_mul_left, image_mul_right, Set.preimage]
  congr! 5 with s hs x
  exact (mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm

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