English
Two lists with nodup and length at least 2 yield disjointness of their formed permutations if and only if the lists are disjoint as sets.
Русский
Два списка без повторений длиной по крайней мере два порождают взаимно непересекающиеся формы перестановок тогда и только тогда, когда сами множества списков непересекаются.
LaTeX
$$$\\text{Perm.Disjoint}(\\text{formPerm } l)(\\text{formPerm } l') \\iff l \\text{Disjoint } l'$$$
Lean4
theorem formPerm_disjoint_iff (hl : Nodup l) (hl' : Nodup l') (hn : 2 ≤ l.length) (hn' : 2 ≤ l'.length) :
Perm.Disjoint (formPerm l) (formPerm l') ↔ l.Disjoint l' :=
by
rw [disjoint_iff_eq_or_eq, List.Disjoint]
constructor
· rintro h x hx hx'
specialize h x
rw [formPerm_apply_mem_eq_self_iff _ hl _ hx, formPerm_apply_mem_eq_self_iff _ hl' _ hx'] at h
cutsat
· intro h x
by_cases hx : x ∈ l
on_goal 1 => by_cases hx' : x ∈ l'
· exact (h hx hx').elim
all_goals have := List.formPerm_apply_of_notMem ‹_›; tauto
