Monotone finite sequences

In this file we prove simp lemmas that allow to simplify propositions like Monotone ![a, b, c].

theorem liftFun_vecCons {α : Type u_1} {n : ℕ} (r : α → α → Prop) [IsTrans α r] {f : Fin (n + 1) → α} {a : α} : ((fun (x x_1 : Fin (Nat.succ (n + 1))) => x < x_1) ⇒ r) (Matrix.vecCons a f) (Matrix.vecCons a f) ↔ r a (f 0) ∧ ((fun (x x_1 : Fin (n + 1)) => x < x_1) ⇒ r) f f

@[simp]

theorem strictMono_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : StrictMono (Matrix.vecCons a f) ↔ a < f 0 ∧ StrictMono f

@[simp]

theorem monotone_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : Monotone (Matrix.vecCons a f) ↔ a ≤ f 0 ∧ Monotone f

@[simp]

theorem monotone_vecEmpty {α : Type u_1} [Preorder α] {a : α} : Monotone ![a]

@[simp]

theorem strictMono_vecEmpty {α : Type u_1} [Preorder α] {a : α} : StrictMono ![a]

@[simp]

theorem strictAnti_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : StrictAnti (Matrix.vecCons a f) ↔ f 0 < a ∧ StrictAnti f

@[simp]

theorem antitone_vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} : Antitone (Matrix.vecCons a f) ↔ f 0 ≤ a ∧ Antitone f

@[simp]

theorem antitone_vecEmpty {α : Type u_1} [Preorder α] {a : α} : Antitone ![a]

@[simp]

theorem strictAnti_vecEmpty {α : Type u_1} [Preorder α] {a : α} : StrictAnti ![a]

theorem StrictMono.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : StrictMono f) (ha : a < f 0) : StrictMono (Matrix.vecCons a f)

theorem StrictAnti.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : StrictAnti f) (ha : f 0 < a) : StrictAnti (Matrix.vecCons a f)

theorem Monotone.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : Monotone f) (ha : a ≤ f 0) : Monotone (Matrix.vecCons a f)

theorem Antitone.vecCons {α : Type u_1} [Preorder α] {n : ℕ} {f : Fin (n + 1) → α} {a : α} (hf : Antitone f) (ha : f 0 ≤ a) : Antitone (Matrix.vecCons a f)