smul_opposite_image_mul_preimage'

English

If S is contained in the normalizer of N, then the product set S*N equals N*S; i.e., S and N commute as sets.

Русский

Если S ⊆ N.normalizer, то S·N = N·S; множества S и N коммутируют.

LaTeX

$$$S N = N S \\quad\\text{if } S \\subseteq N.\\mathrm{normalizer}$$$

Lean4

@[to_additive]
theorem smul_opposite_image_mul_preimage' (g : G) (h : Gᵐᵒᵖ) (s : Set G) :
    (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s) := by
  simp [preimage_preimage, mul_assoc]
    -- TODO: deprecate?

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