triplewise_iff_getElem — Mathlib

English

For a list l and a ternary predicate p, l is triplewise with respect to p if and only if for all indices i < j < k with k < length(l), p l[i] l[j] l[k] holds.

Русский

Для списка l и тройного предиката p условие тройственности эквивалентно тому, что для всех индексов i < j < k с k < длина(l) верно p l[i] l[j] l[k].

LaTeX

$$$l.\text{Triplewise } p \;\iff\; \forall i\,j\,k\ (hij: i

Lean4

theorem triplewise_iff_getElem :
    l.Triplewise p ↔ ∀ i j k (hij : i < j) (hjk : j < k) (hk : k < l.length), p l[i] l[j] l[k] := by
  induction l with
  | nil => simp
  | cons head tail ih =>
    simp only [triplewise_cons, length_cons, pairwise_iff_getElem, ih]
    refine ⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_, fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩
    · grind
    · simpa using h 0 (i + 1) (j + 1) (by cutsat) (by cutsat) (by cutsat)
    · simpa using h (i + 1) (j + 1) (k + 1) (by cutsat) (by cutsat) (by cutsat)

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