English
For all α,β, r, and lists l, u, v, if l is a permutation of u and u is Forall₂-related to v, then the two natural compositions of Forall₂ and Perm are equal as relations: Forall₂ r ∘r Perm = Perm ∘r Forall₂ r.
Русский
Для всех α,β, r и списков l,u,v, если l перестановочно эквивален u, а u связана с v отношением Forall₂, то композиции этих отношений равны: Forall₂ r ∘r Perm = Perm ∘r Forall₂ r.
LaTeX
$$$\\mathrm{Forall}_2(r) \\circ_r \\mathrm{Perm} = \\mathrm{Perm} \\circ_r \\mathrm{Forall}_2(r)$$$
Lean4
theorem forall₂_comp_perm_eq_perm_comp_forall₂ : Forall₂ r ∘r Perm = Perm ∘r Forall₂ r :=
by
funext l₁ l₃; apply propext
constructor
· intro h
rcases h with ⟨l₂, h₁₂, h₂₃⟩
have : Forall₂ (flip r) l₂ l₁ := h₁₂.flip
rcases perm_comp_forall₂ h₂₃.symm this with ⟨l', h₁, h₂⟩
exact ⟨l', h₂.symm, h₁.flip⟩
· exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃
