English
Let l1, l2, t1, t2 be lists. If l1 is a permutation of l2 and t1 is a permutation of t2, then the multisets obtained by intersecting l1 with t1 and l2 with t2 are themselves permutations of each other.
Русский
Пусть списки l1, l2, t1, t2 удовлетворяют: l1 перестановочно эквивален l2 и t1 перестановочно эквивален t2. Тогда их мульти пересечения l1 ∩ t1 и l2 ∩ t2 равноперемещаются, то есть являются перестановками друг друга.
LaTeX
$$$\forall \{\alpha\}, \text{DecidableEq}(\alpha)\; l_1, l_2, t_1, t_2 : List\alpha,\; l_1 \sim l_2 \land t_1 \sim t_2 \Rightarrow (l_1 \bagInter t_1) \sim (l_2 \bagInter t_2)$$$
Lean4
theorem bagInter {l₁ l₂ t₁ t₂ : List α} (hl : l₁ ~ l₂) (ht : t₁ ~ t₂) : l₁.bagInter t₁ ~ l₂.bagInter t₂ :=
ht.bagInter_left l₂ ▸ hl.bagInter_right _
