triplewise_map — Mathlib

English

Mapping a function f over a list preserves a transformed triplewise predicate: (l.map f).Triplewise p' iff l.Triplewise (λ a b c, p'(f a)(f b)(f c)).

Русский

Преобразование списка функцией f сохраняет тройной тройной характер: (l.map f).Triplewise p' эквивалентно l.Triplewise (λ a b c, p'(f a)(f b)(f c)).

LaTeX

$$$$ (l.map f).Triplewise\\, p' \\iff l.Triplewise (\\lambda a b c. p' (f a) (f b) (f c)) $$$$

Lean4

theorem triplewise_map : (l.map f).Triplewise p' ↔ l.Triplewise (fun a b c ↦ p' (f a) (f b) (f c)) := by
  induction l with
  | nil => simp
  | cons h t ih => simp [map, triplewise_cons, ih, pairwise_map]

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