stabilizer_union_eq_right — Mathlib

English

If s and t are disjoint and stabilizers are nested oppositely, then stabilizer of the union equals stabilizer of t.

Русский

Если s и t дизъюнкты и вложения стабилизаторов противоположны, то стабилизатор объединения равен стабилизатору t.

LaTeX

$$$ \operatorname{Stab}_G(s \cup t) = \operatorname{Stab}_G(t) \,$ under the stated hypotheses$$

Lean4

@[to_additive]
theorem stabilizer_union_eq_right (hdisj : Disjoint s t) (hstab : stabilizer G t ≤ stabilizer G s)
    (hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G s) : stabilizer G (s ∪ t) = stabilizer G t := by
  rw [union_comm, stabilizer_union_eq_left hdisj.symm hstab (union_comm .. ▸ hstab_union)]

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