English
Let l be a finite list of pairwise disjoint permutations of α, and suppose f is one of the elements of l. Then for every x in the support of f, f(x) equals the product of the elements of l applied to x.
Русский
Пусть l — конечный список перестановок α попарно нес пересекающихся, и пусть f ∈ l. Тогда для каждого x из опоры f выполняется f(x) = (l.prod)(x).
LaTeX
$$$\forall x \in \operatorname{supp}(f),\ f(x) = \left(\prod_{\sigma \in l} \sigma\right)(x)\quad\text{при условии } f \in l\ \text{и } l\text{ Pairwise Disjoint}$$$
Lean4
theorem eq_on_support_mem_disjoint {l : List (Perm α)} (h : f ∈ l) (hl : l.Pairwise Disjoint) :
∀ x ∈ f.support, f x = l.prod x := by
induction l with
| nil => simp at h
| cons hd tl IH =>
intro x hx
rw [List.pairwise_cons] at hl
rw [List.mem_cons] at h
rcases h with (rfl | h)
· rw [List.prod_cons, mul_apply, notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
· rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← notMem_support]
refine (hl.left _ h).symm.mem_imp ?_
simpa using hx
