stabilizer_inf_stabilizer_le_stabilizer_union

English

The intersection of the stabilizers of s and t is contained in the stabilizer of their union.

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem stabilizer_inf_stabilizer_le_stabilizer_union : stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (s ∪ t) :=
  stabilizer_inf_stabilizer_le_stabilizer_apply₂ fun _ ↦ smul_set_union

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