triplewise_cons — Mathlib

English

Adding an element to the front of a list relates its triplewise property to the triplewise of the tail and the pairwise of the tail with p(a, ·).

Русский

Добавление элемента вперед списка связывает его свойство triplewise с тройной последовательностью хвоста и попарностью хвоста относительно p a.

LaTeX

$$$$ (a :: l).Triplewise\\, p \\iff l.Pairwise\\,(p\\,a) \\land l.Triplewise\\, p. $$$$

Lean4

@[grind =]
theorem triplewise_cons : (a :: l).Triplewise p ↔ l.Pairwise (p a) ∧ l.Triplewise p := by rw [triplewise_iff]; aesop

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