mathlib documentation

data.fin.tuple.monotone

Monotone finite sequences #

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 : α} :
(has_lt.lt r) (matrix.vec_cons a f) (matrix.vec_cons a f) r a (f 0) (has_lt.lt r) f f
@[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) :