mathlib documentation

algebra.order_functions

max and min

This file proves basic properties about maxima and minima on a decidable_linear_order.

Tags

min, max

@[simp]
theorem le_min_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
c min a b c a c b

@[simp]
theorem max_le_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
max a b c a c b c

theorem max_le_max {α : Type u} [decidable_linear_order α] {a b c d : α} :
a cb dmax a b max c d

theorem min_le_min {α : Type u} [decidable_linear_order α] {a b c d : α} :
a cb dmin a b min c d

theorem le_max_left_of_le {α : Type u} [decidable_linear_order α] {a b c : α} :
a ba max b c

theorem le_max_right_of_le {α : Type u} [decidable_linear_order α] {a b c : α} :
a ca max b c

theorem min_le_left_of_le {α : Type u} [decidable_linear_order α] {a b c : α} :
a cmin a b c

theorem min_le_right_of_le {α : Type u} [decidable_linear_order α] {a b c : α} :
b cmin a b c

theorem max_min_distrib_left {α : Type u} [decidable_linear_order α] {a b c : α} :
max a (min b c) = min (max a b) (max a c)

theorem max_min_distrib_right {α : Type u} [decidable_linear_order α] {a b c : α} :
max (min a b) c = min (max a c) (max b c)

theorem min_max_distrib_left {α : Type u} [decidable_linear_order α] {a b c : α} :
min a (max b c) = max (min a b) (min a c)

theorem min_max_distrib_right {α : Type u} [decidable_linear_order α] {a b c : α} :
min (max a b) c = max (min a c) (min b c)

theorem min_le_max {α : Type u} [decidable_linear_order α] {a b : α} :
min a b max a b

@[instance]
def max_idem {α : Type u} [decidable_linear_order α] :

An instance asserting that max a a = a

@[instance]
def min_idem {α : Type u} [decidable_linear_order α] :

An instance asserting that min a a = a

@[simp]
theorem max_lt_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
max a b < c a < c b < c

@[simp]
theorem lt_min_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
a < min b c a < b a < c

@[simp]
theorem lt_max_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
a < max b c a < b a < c

@[simp]
theorem min_lt_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
min a b < c a < c b < c

@[simp]
theorem min_le_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
min a b c a c b c

@[simp]
theorem le_max_iff {α : Type u} [decidable_linear_order α] {a b c : α} :
a max b c a b a c

theorem max_lt_max {α : Type u} [decidable_linear_order α] {a b c d : α} :
a < cb < dmax a b < max c d

theorem min_lt_min {α : Type u} [decidable_linear_order α] {a b c d : α} :
a < cb < dmin a b < min c d

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

theorem max.left_comm {α : Type u} [decidable_linear_order α] (a b c : α) :
max a (max b c) = max b (max a c)

theorem max.right_comm {α : Type u} [decidable_linear_order α] (a b c : α) :
max (max a b) c = max (max a c) b

theorem monotone.map_max {α : Type u} {β : Type v} [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b : α} :
monotone ff (max a b) = max (f a) (f b)

theorem monotone.map_min {α : Type u} {β : Type v} [decidable_linear_order α] [decidable_linear_order β] {f : α → β} {a b : α} :
monotone ff (min a b) = min (f a) (f b)

theorem min_choice {α : Type u} [decidable_linear_order α] (a b : α) :
min a b = a min a b = b

theorem max_choice {α : Type u} [decidable_linear_order α] (a b : α) :
max a b = a max a b = b

theorem le_of_max_le_left {α : Type u} [decidable_linear_order α] {a b c : α} :
max a b ca c

theorem le_of_max_le_right {α : Type u} [decidable_linear_order α] {a b c : α} :
max a b cb c