English
For any set S of permutations, any element a in the closure of S has its support contained in the union of supports of elements of S.
Русский
Для множества S перестановок любой элемент a в замыкании S имеет поддержку, включающуюся в объединение поддержек элементов S.
LaTeX
$$$a \\in \\overline{S} \\Rightarrow \\operatorname{supp}(a) \\subseteq \\bigcup_{b \\in S} \\operatorname{supp}(b).$$$
Lean4
theorem support_closure_subset_union (S : Set (Perm α)) : ∀ a ∈ closure S, (a.support : Set α) ⊆ ⋃ b ∈ S, b.support :=
by
apply closure_induction
· exact fun x hx ↦ Set.subset_iUnion₂_of_subset x hx subset_rfl
· simp only [support_one, Finset.coe_empty, Set.empty_subset]
· intro a b ha hb hc hd
refine (Finset.coe_subset.mpr (support_mul_le a b)).trans ?_
rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]
exact ⟨hc, hd⟩
· simp only [support_inv, imp_self, implies_true]
