Monotone finite sequences #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem lift_fun_vec_cons {α : Type u_1} {n : ℕ} (r : α → α → Prop) [is_trans α r] {f : fin (n + 1) → α} {a : α} :

@[simp]

theorem strict_mono_vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} :

@[simp]

theorem monotone_vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} :

@[simp]

theorem strict_anti_vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} :

@[simp]

theorem antitone_vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} :

theorem strict_mono.vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} (hf : strict_mono f) (ha : a < f 0) :

theorem strict_anti.vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} (hf : strict_anti f) (ha : f 0 < a) :

theorem monotone.vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} (hf : monotone f) (ha : a ≤ f 0) :

theorem antitone.vec_cons {α : Type u_1} [preorder α] {n : ℕ} {f : fin (n + 1) → α} {a : α} (hf : antitone f) (ha : f 0 ≤ a) :