stabilizer_mul_self — Mathlib

English

For any set s ⊆ G, the product of the stabilizer of s with s (on the left) yields s.

Русский

Для множества s ⊆ G произведение стабилизатора s с s слева даёт множество s.

LaTeX

$$$ (\operatorname{Stab}_G(s) : \operatorname{Set} G) \cdot s = s $$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_mul_self (s : Set G) : (stabilizer G s : Set G) * s = s :=
  by
  ext
  refine ⟨?_, fun h ↦ ⟨_, (stabilizer G s).one_mem, _, h, one_mul _⟩⟩
  rintro ⟨a, ha, b, hb, rfl⟩
  rw [← mem_stabilizer_iff.1 ha]
  exact smul_mem_smul_set hb

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