mathlib documentation

core.init.algebra.functions

def min {α : Type u} [linear_order α] :
α → α → α

Equations
def max {α : Type u} [linear_order α] :
α → α → α

Equations
theorem min_le_left {α : Type u} [linear_order α] (a b : α) :
min a b a

theorem min_le_right {α : Type u} [linear_order α] (a b : α) :
min a b b

theorem le_min {α : Type u} [linear_order α] {a b c : α} :
c ac bc min a b

theorem le_max_left {α : Type u} [linear_order α] (a b : α) :
a max a b

theorem le_max_right {α : Type u} [linear_order α] (a b : α) :
b max a b

theorem max_le {α : Type u} [linear_order α] {a b c : α} :
a cb cmax a b c

theorem eq_min {α : Type u} [linear_order α] {a b c : α} :
c ac b(∀ {d : α}, d ad bd c)c = min a b

theorem min_comm {α : Type u} [linear_order α] (a b : α) :
min a b = min b a

theorem min_assoc {α : Type u} [linear_order α] (a b c : α) :
min (min a b) c = min a (min b c)

theorem min_left_comm {α : Type u} [linear_order α] (a b c : α) :
min a (min b c) = min b (min a c)

@[simp]
theorem min_self {α : Type u} [linear_order α] (a : α) :
min a a = a

@[simp]
theorem min_eq_left {α : Type u} [linear_order α] {a b : α} :
a bmin a b = a

@[simp]
theorem min_eq_right {α : Type u} [linear_order α] {a b : α} :
b amin a b = b

theorem eq_max {α : Type u} [linear_order α] {a b c : α} :
a cb c(∀ {d : α}, a db dc d)c = max a b

theorem max_comm {α : Type u} [linear_order α] (a b : α) :
max a b = max b a

theorem max_assoc {α : Type u} [linear_order α] (a b c : α) :
max (max a b) c = max a (max b c)

theorem max_left_comm {α : Type u} [linear_order α] (a b c : α) :
max a (max b c) = max b (max a c)

@[simp]
theorem max_self {α : Type u} [linear_order α] (a : α) :
max a a = a

@[simp]
theorem max_eq_left {α : Type u} [linear_order α] {a b : α} :
b amax a b = a

@[simp]
theorem max_eq_right {α : Type u} [linear_order α] {a b : α} :
a bmax a b = b

theorem min_eq_left_of_lt {α : Type u} [linear_order α] {a b : α} :
a < bmin a b = a

theorem min_eq_right_of_lt {α : Type u} [linear_order α] {a b : α} :
b < amin a b = b

theorem max_eq_left_of_lt {α : Type u} [linear_order α] {a b : α} :
b < amax a b = a

theorem max_eq_right_of_lt {α : Type u} [linear_order α] {a b : α} :
a < bmax a b = b

theorem lt_min {α : Type u} [linear_order α] {a b c : α} :
a < ba < ca < min b c

theorem max_lt {α : Type u} [linear_order α] {a b c : α} :
a < cb < cmax a b < c