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 α} : 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 α} : 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 (Array.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}, Array.Pairwise R #[]

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

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

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

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

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