stabilizer_inf_stabilizer_le_stabilizer_apply₂

English

If a function f on sets respects the action, then the intersection of stabilizers of s and t is contained in the stabilizer of f(s,t).

Русский

Если функция f по множествам сохраняет действие, тогда пересечение стабилизаторов s и t содержится в стабилизаторе f(s,t).

LaTeX

$$$ \Bigl( \operatorname{Stab}_G(s) \cap \operatorname{Stab}_G(t) \Bigr) \le \operatorname{Stab}_G( f(s,t) ) \,,$$$

Lean4

@[to_additive]
theorem stabilizer_inf_stabilizer_le_stabilizer_apply₂ {f : Set α → Set α → Set α}
    (hf : ∀ a : G, a • f s t = f (a • s) (a • t)) : stabilizer G s ⊓ stabilizer G t ≤ stabilizer G (f s t) := by
  aesop (add simp [SetLike.le_def])

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