max and min#

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

Tags #

min, max

@[simp]
theorem le_min_iff {α : Type u} [] {a : α} {b : α} {c : α} :
c min a b c a c b
@[simp]
theorem le_max_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a max b c a b a c
@[simp]
theorem min_le_iff {α : Type u} [] {a : α} {b : α} {c : α} :
min a b c a c b c
@[simp]
theorem max_le_iff {α : Type u} [] {a : α} {b : α} {c : α} :
max a b c a c b c
@[simp]
theorem lt_min_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a < min b c a < b a < c
@[simp]
theorem lt_max_iff {α : Type u} [] {a : α} {b : α} {c : α} :
a < max b c a < b a < c
@[simp]
theorem min_lt_iff {α : Type u} [] {a : α} {b : α} {c : α} :
min a b < c a < c b < c
@[simp]
theorem max_lt_iff {α : Type u} [] {a : α} {b : α} {c : α} :
max a b < c a < c b < c
theorem max_le_max {α : Type u} [] {a : α} {b : α} {c : α} {d : α} :
a cb dmax a b max c d
theorem max_le_max_left {α : Type u} [] {a : α} {b : α} (c : α) (h : a b) :
max c a max c b
theorem max_le_max_right {α : Type u} [] {a : α} {b : α} (c : α) (h : a b) :
max a c max b c
theorem min_le_min {α : Type u} [] {a : α} {b : α} {c : α} {d : α} :
a cb dmin a b min c d
theorem min_le_min_left {α : Type u} [] {a : α} {b : α} (c : α) (h : a b) :
min c a min c b
theorem min_le_min_right {α : Type u} [] {a : α} {b : α} (c : α) (h : a b) :
min a c min b c
theorem le_max_of_le_left {α : Type u} [] {a : α} {b : α} {c : α} :
a ba max b c
theorem le_max_of_le_right {α : Type u} [] {a : α} {b : α} {c : α} :
a ca max b c
theorem lt_max_of_lt_left {α : Type u} [] {a : α} {b : α} {c : α} (h : a < b) :
a < max b c
theorem lt_max_of_lt_right {α : Type u} [] {a : α} {b : α} {c : α} (h : a < c) :
a < max b c
theorem min_le_of_left_le {α : Type u} [] {a : α} {b : α} {c : α} :
a cmin a b c
theorem min_le_of_right_le {α : Type u} [] {a : α} {b : α} {c : α} :
b cmin a b c
theorem min_lt_of_left_lt {α : Type u} [] {a : α} {b : α} {c : α} (h : a < c) :
min a b < c
theorem min_lt_of_right_lt {α : Type u} [] {a : α} {b : α} {c : α} (h : b < c) :
min a b < c
theorem max_min_distrib_left {α : Type u} [] (a : α) (b : α) (c : α) :
max a (min b c) = min (max a b) (max a c)
theorem max_min_distrib_right {α : Type u} [] (a : α) (b : α) (c : α) :
max (min a b) c = min (max a c) (max b c)
theorem min_max_distrib_left {α : Type u} [] (a : α) (b : α) (c : α) :
min a (max b c) = max (min a b) (min a c)
theorem min_max_distrib_right {α : Type u} [] (a : α) (b : α) (c : α) :
min (max a b) c = max (min a c) (min b c)
theorem min_le_max {α : Type u} [] {a : α} {b : α} :
min a b max a b
@[simp]
theorem min_eq_left_iff {α : Type u} [] {a : α} {b : α} :
min a b = a a b
@[simp]
theorem min_eq_right_iff {α : Type u} [] {a : α} {b : α} :
min a b = b b a
@[simp]
theorem max_eq_left_iff {α : Type u} [] {a : α} {b : α} :
max a b = a b a
@[simp]
theorem max_eq_right_iff {α : Type u} [] {a : α} {b : α} :
max a b = b a b
theorem min_cases {α : Type u} [] (a : α) (b : α) :
min a b = a a b min a b = b b < a

For elements a and b of a linear order, either min a b = a and a ≤ b, or min a b = b and b < a. Use cases on this lemma to automate linarith in inequalities

theorem max_cases {α : Type u} [] (a : α) (b : α) :
max a b = a b a max a b = b a < b

For elements a and b of a linear order, either max a b = a and b ≤ a, or max a b = b and a < b. Use cases on this lemma to automate linarith in inequalities

theorem min_eq_iff {α : Type u} [] {a : α} {b : α} {c : α} :
min a b = c a = c a b b = c b a
theorem max_eq_iff {α : Type u} [] {a : α} {b : α} {c : α} :
max a b = c a = c b a b = c a b
theorem min_lt_min_left_iff {α : Type u} [] {a : α} {b : α} {c : α} :
min a c < min b c a < b a < c
theorem min_lt_min_right_iff {α : Type u} [] {a : α} {b : α} {c : α} :
min a b < min a c b < c b < a
theorem max_lt_max_left_iff {α : Type u} [] {a : α} {b : α} {c : α} :
max a c < max b c a < b c < b
theorem max_lt_max_right_iff {α : Type u} [] {a : α} {b : α} {c : α} :
max a b < max a c b < c a < c
instance max_idem {α : Type u} [] :

An instance asserting that max a a = a

Equations
• =
instance min_idem {α : Type u} [] :

An instance asserting that min a a = a

Equations
• =
theorem min_lt_max {α : Type u} [] {a : α} {b : α} :
min a b < max a b a b
theorem max_lt_max {α : Type u} [] {a : α} {b : α} {c : α} {d : α} (h₁ : a < c) (h₂ : b < d) :
max a b < max c d
theorem min_lt_min {α : Type u} [] {a : α} {b : α} {c : α} {d : α} (h₁ : a < c) (h₂ : b < d) :
min a b < min c d
theorem min_right_comm {α : Type u} [] (a : α) (b : α) (c : α) :
min (min a b) c = min (min a c) b
theorem Max.left_comm {α : Type u} [] (a : α) (b : α) (c : α) :
max a (max b c) = max b (max a c)
theorem Max.right_comm {α : Type u} [] (a : α) (b : α) (c : α) :
max (max a b) c = max (max a c) b
theorem MonotoneOn.map_max {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {b : α} (hf : ) (ha : a s) (hb : b s) :
f (max a b) = max (f a) (f b)
theorem MonotoneOn.map_min {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {b : α} (hf : ) (ha : a s) (hb : b s) :
f (min a b) = min (f a) (f b)
theorem AntitoneOn.map_max {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {b : α} (hf : ) (ha : a s) (hb : b s) :
f (max a b) = min (f a) (f b)
theorem AntitoneOn.map_min {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {b : α} (hf : ) (ha : a s) (hb : b s) :
f (min a b) = max (f a) (f b)
theorem Monotone.map_max {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
f (max a b) = max (f a) (f b)
theorem Monotone.map_min {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
f (min a b) = min (f a) (f b)
theorem Antitone.map_max {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
f (max a b) = min (f a) (f b)
theorem Antitone.map_min {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} {b : α} (hf : ) :
f (min a b) = max (f a) (f b)
theorem min_choice {α : Type u} [] (a : α) (b : α) :
min a b = a min a b = b
theorem max_choice {α : Type u} [] (a : α) (b : α) :
max a b = a max a b = b
theorem le_of_max_le_left {α : Type u} [] {a : α} {b : α} {c : α} (h : max a b c) :
a c
theorem le_of_max_le_right {α : Type u} [] {a : α} {b : α} {c : α} (h : max a b c) :
b c
instance instCommutativeMax {α : Type u} [] :
Equations
• =
instance instAssociativeMax {α : Type u} [] :
Equations
• =
instance instCommutativeMin {α : Type u} [] :
Equations
• =
instance instAssociativeMin {α : Type u} [] :
Equations
• =
theorem max_left_commutative {α : Type u} [] :
theorem min_left_commutative {α : Type u} [] :
@[deprecated instCommutativeMax]
theorem max_commutative {α : Type u} [] :
@[deprecated instAssociativeMax]
theorem max_associative {α : Type u} [] :
@[deprecated instCommutativeMin]
theorem min_commutative {α : Type u} [] :
@[deprecated instAssociativeMin]
theorem min_associative {α : Type u} [] :