stabilizer_inf_stabilizer_le_stabilizer_sdiff

English

The intersection of stabilizers is contained in the stabilizer of the set difference s \ t.

Русский

Пересечение стабилизаторов содержится в стабилизаторе множества различия s \ t.

LaTeX

$$$ \operatorname{Stab}_G(s) \cap \operatorname{Stab}_G(t) \le \operatorname{Stab}_G(s \setminus t) $$$

Lean4

@[to_additive]
theorem stabilizer_inf_stabilizer_le_stabilizer_sdiff : stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s \ t) :=
  stabilizer_inf_stabilizer_le_stabilizer_apply₂ fun _ ↦ smul_set_sdiff

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