English
If s and t are disjoint and stabilizers are nested in a certain way, then stabilizer of the union equals stabilizer of s.
Русский
Если s и t дизъюнкты и выполняются условия вложенности стабилизаторов, то стабилизатор объединения равен стабилизатору s.
LaTeX
$$$ Disjoint(s,t) \land (\operatorname{Stab}_G(s) \le \operatorname{Stab}_G(t)) \land (\operatorname{Stab}_G(s \cup t) \le \operatorname{Stab}_G(t)) \Rightarrow \operatorname{Stab}_G(s \cup t) = \operatorname{Stab}_G(s) $$$
Lean4
@[to_additive]
theorem stabilizer_union_eq_left (hdisj : Disjoint s t) (hstab : stabilizer G s ≤ stabilizer G t)
(hstab_union : stabilizer G (s ∪ t) ≤ stabilizer G t) : stabilizer G (s ∪ t) = stabilizer G s :=
by
refine le_antisymm ?_ ?_
·
calc
stabilizer G (s ∪ t) ≤ stabilizer G (s ∪ t) ⊓ stabilizer G t := by simpa
_ ≤ stabilizer G ((s ∪ t) \ t) := stabilizer_inf_stabilizer_le_stabilizer_sdiff
_ = stabilizer G s := by rw [union_diff_cancel_right]; simpa [← disjoint_iff_inter_eq_empty]
·
calc
stabilizer G s ≤ stabilizer G s ⊓ stabilizer G t := by simpa
_ ≤ stabilizer G (s ∪ t) := stabilizer_inf_stabilizer_le_stabilizer_union
