English
If l is a list of pairwise disjoint permutations, then the support of the product l.prod equals the join (sup) of the individual supports along the list.
Русский
Если список l состоит из попарно несовместимых перестановок, то опора произведения l.prod равна объединению опор по списку.
LaTeX
$$$l.prod.\operatorname{support} = \bigcup_{f\in l} \operatorname{support}(f)$ (in the join sense).$$
Lean4
theorem support_mul (h : Disjoint f g) : (f * g).support = f.support ∪ g.support :=
by
refine le_antisymm (support_mul_le _ _) fun a => ?_
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
exact
(h a).elim (fun hf h => ⟨hf, f.apply_eq_iff_eq.mp (h.trans hf.symm)⟩) fun hg h =>
⟨(congr_arg f hg).symm.trans h, hg⟩
