Pairwise

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.Pairwise

Lean4

/-- `Pairwise R s` means that all the elements with earlier indices are
`R`-related to all the elements with later indices.
```
Pairwise R [1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3
```
For example if `R = (· ≠ ·)` then it asserts `s` has no duplicates,
and if `R = (· < ·)` then it asserts that `s` is (strictly) sorted.
-/
def Pairwise (R : α → α → Prop) (s : Seq α) : Prop :=
  ∀ i j, i < j → ∀ x ∈ s.get? i, ∀ y ∈ s.get? j, R x y

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

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

Разделы

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

Аффилиация

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