def Array.Pairwise {α : Type u_1} (R : α → α → Prop) (as : Array α) : Prop

Pairwise R as means that all the elements of the array as are R-related to all elements with larger indices.

Pairwise R #[1, 2, 3] ↔ R 1 2 ∧ R 1 3 ∧ R 2 3

For example as.Pairwise (· ≠ ·) asserts that as has no duplicates, as.Pairwise (· < ·) asserts that as is strictly sorted and as.Pairwise (· ≤ ·) asserts that as is weakly sorted.

Equations

• Array.Pairwise R as = List.Pairwise R as.toList

theorem Array.pairwise_iff_get {α : Type u_1} {R : α → α → Prop} {as : Array α} : Pairwise R as ↔ ∀ (i j : Fin as.size), i < j → R (as.get ↑i ⋯) (as.get ↑j ⋯)

theorem Array.pairwise_iff_getElem {α : Type u_1} {R : α → α → Prop} {as : Array α} : Pairwise R as ↔ ∀ (i j : Nat) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]

instance Array.instDecidablePairwiseOfDecidableRel {α : Type u_1} (R : α → α → Prop) [DecidableRel R] (as : Array α) : Decidable (Pairwise R as)

Equations

• Array.instDecidablePairwiseOfDecidableRel R as = decidable_of_iff (∀ (j : Fin as.size) (i : Fin ↑j), R as[↑i] as[↑j]) ⋯

theorem Array.pairwise_empty {α✝ : Type u_1} {R : α✝ → α✝ → Prop} : Pairwise R #[]

theorem Array.pairwise_singleton {α : Type u_1} (R : α → α → Prop) (a : α) : Pairwise R #[a]

theorem Array.pairwise_pair {α✝ : Type u_1} {a b : α✝} {R : α✝ → α✝ → Prop} : Pairwise R #[a, b] ↔ R a b

theorem Array.pairwise_append {α : Type u_1} {R : α → α → Prop} {as bs : Array α} : Pairwise R (as ++ bs) ↔ Pairwise R as ∧ Pairwise R bs ∧ ∀ (x : α), x ∈ as → ∀ (y : α), y ∈ bs → R x y

theorem Array.pairwise_push {α : Type u_1} {a : α} {R : α → α → Prop} {as : Array α} : Pairwise R (as.push a) ↔ Pairwise R as ∧ ∀ (x : α), x ∈ as → R x a

theorem Array.pairwise_extract {α : Type u_1} {R : α → α → Prop} {as : Array α} (h : Pairwise R as) (start stop : Nat) : Pairwise R (as.extract start stop)