English
For p a ternary predicate, the triplewise property of l1 ++ l2 is equivalent to l1 triplewise p, l2 triplewise p, and certain compatibility conditions between l1 and l2: every a in l1 is pairwise with l2 under p, and for every a in l2, l1 is pairwise with the slice of p determined by a.
Русский
Для тройного предиката p тройственность списка l1 ++ l2 эквивалентна тройственности l1 по p, тройственности l2 по p и условиям совместимости между l1 и l2: каждый элемент из l1 совместим с l2 под p, а каждый элемент из l2 совместим с l1 через соответствующую зависимую пару.
LaTeX
$$$ (l_1 \!\!\! l_2).Triplewise p \\iff \\ (l_1.Triplewise p) \land (l_2.Triplewise p) \land (\\forall a \in l_1, \, l_2.\text{Pairwise } (p\ a)) \\land (\\forall a \in l_2, \, l_1.\text{Pairwise } (\\lambda x y, p x y a))$$$
Lean4
theorem triplewise_append :
(l₁ ++ l₂).Triplewise p ↔
l₁.Triplewise p ∧ l₂.Triplewise p ∧ (∀ a ∈ l₁, l₂.Pairwise (p a)) ∧ ∀ a ∈ l₂, l₁.Pairwise fun x y ↦ p x y a :=
by
induction l₁ with
| nil => simp
| cons h t ih =>
simp [triplewise_cons, ih, pairwise_append]
aesop
