triplewise_reverse — Mathlib

English

Reversing a list converts triplewise p to triplewise with p reversed: l.reverse is triplewise under p' if l is triplewise under p, where p'(a,b,c) := p c b a.

Русский

Обращение списка превращает тройственность: если l тройственно относительно p, то l.reverse тройственно относительно p' с p'(a,b,c) := p(c,b,a).

LaTeX

$$$l.\text{Triplewise } p \iff l.\text{Triplewise } (\\lambda a\,b\,c, p\, c\, b\, a)$$$

Lean4

theorem triplewise_reverse : l.reverse.Triplewise p ↔ l.Triplewise fun a b c ↦ p c b a := by
  induction l with
  | nil => simp
  | cons h t ih => simp [triplewise_append, pairwise_reverse, triplewise_cons, ih, and_comm]

Похожие утверждения