Triplewise

Mathlib.Data.List.Triplewise

URI: https://scilib.ai/kg/mathlib#List.Triplewise

Lean4

/-- Whether a predicate holds for all ordered triples of elements of a list. -/
@[mk_iff]
inductive Triplewise (p : α → α → α → Prop) : List α → Prop
  | nil : [].Triplewise p
  | cons {a : α} {l : List α} : l.Pairwise (p a) → l.Triplewise p → (a :: l).Triplewise p

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru