English
Let l be a list of α, let p be a ternary predicate on α, and f: α → β. If for all a,b,c we have p a b c → p'(f a) (f b) (f c), and l is triplewise with respect to p, then l mapped by f is triplewise with respect to p'.
Русский
Пусть l — список элементов из α, p — тройной предикат на α, и f: α → β. Если для любых a,b,c верно p a b c ⇒ p'(f a) (f b) (f c), и l является тройственным относительно p, то l → f является тройственным относительно p'.
LaTeX
$$$\big(\forall a\,b\,c\,\ p\ a\ b\ c \to p'(f\ a)\ (f\ b)\ (f\ c)\big)\ \to\ l\.Triplewise p\ \to\ (l\.map f)\.Triplewise p'$$$
Lean4
theorem map (h : ∀ {a b c}, p a b c → p' (f a) (f b) (f c)) (hl : l.Triplewise p) : (l.map f).Triplewise p' :=
triplewise_map.2 (hl.imp h)
