order.min_max

# max and min#

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

## Tags #

min, max

@[simp]
theorem le_min_iff {α : Type u} [linear_order α] {a b c : α} :
c c a c b
@[simp]
theorem le_max_iff {α : Type u} [linear_order α] {a b c : α} :
a a b a c
@[simp]
theorem min_le_iff {α : Type u} [linear_order α] {a b c : α} :
c a c b c
@[simp]
theorem max_le_iff {α : Type u} [linear_order α] {a b c : α} :
c a c b c
@[simp]
theorem lt_min_iff {α : Type u} [linear_order α] {a b c : α} :
a < a < b a < c
@[simp]
theorem lt_max_iff {α : Type u} [linear_order α] {a b c : α} :
a < a < b a < c
@[simp]
theorem min_lt_iff {α : Type u} [linear_order α] {a b c : α} :
< c a < c b < c
@[simp]
theorem max_lt_iff {α : Type u} [linear_order α] {a b c : α} :
< c a < c b < c
theorem max_le_max {α : Type u} [linear_order α] {a b c d : α} :
a cb d
theorem min_le_min {α : Type u} [linear_order α] {a b c d : α} :
a cb d
theorem le_max_of_le_left {α : Type u} [linear_order α] {a b c : α} :
a ba
theorem le_max_of_le_right {α : Type u} [linear_order α] {a b c : α} :
a ca
theorem lt_max_of_lt_left {α : Type u} [linear_order α] {a b c : α} (h : a < b) :
a <
theorem lt_max_of_lt_right {α : Type u} [linear_order α] {a b c : α} (h : a < c) :
a <
theorem min_le_of_left_le {α : Type u} [linear_order α] {a b c : α} :
a c c
theorem min_le_of_right_le {α : Type u} [linear_order α] {a b c : α} :
b c c
theorem min_lt_of_left_lt {α : Type u} [linear_order α] {a b c : α} (h : a < c) :
< c
theorem min_lt_of_right_lt {α : Type u} [linear_order α] {a b c : α} (h : b < c) :
< c
theorem max_min_distrib_left {α : Type u} [linear_order α] {a b c : α} :
c) = c)
theorem max_min_distrib_right {α : Type u} [linear_order α] {a b c : α} :
c = c)
theorem min_max_distrib_left {α : Type u} [linear_order α] {a b c : α} :
c) = c)
theorem min_max_distrib_right {α : Type u} [linear_order α] {a b c : α} :
c = c)
theorem min_le_max {α : Type u} [linear_order α] {a b : α} :
@[simp]
theorem min_eq_left_iff {α : Type u} [linear_order α] {a b : α} :
= a a b
@[simp]
theorem min_eq_right_iff {α : Type u} [linear_order α] {a b : α} :
= b b a
@[simp]
theorem max_eq_left_iff {α : Type u} [linear_order α] {a b : α} :
= a b a
@[simp]
theorem max_eq_right_iff {α : Type u} [linear_order α] {a b : α} :
= b a b
theorem min_cases {α : Type u} [linear_order α] (a b : α) :
= a 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} [linear_order α] (a b : α) :
= a b a = 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} [linear_order α] {a b c : α} :
= c a = c a b b = c b a
theorem max_eq_iff {α : Type u} [linear_order α] {a b c : α} :
= c a = c b a b = c a b
theorem min_lt_min_left_iff {α : Type u} [linear_order α] {a b c : α} :
a < b a < c
theorem min_lt_min_right_iff {α : Type u} [linear_order α] {a b c : α} :
b < c b < a
theorem max_lt_max_left_iff {α : Type u} [linear_order α] {a b c : α} :
a < b c < b
theorem max_lt_max_right_iff {α : Type u} [linear_order α] {a b c : α} :
b < c a < c
@[protected, instance]
def max_idem {α : Type u} [linear_order α] :

An instance asserting that max a a = a

@[protected, instance]
def min_idem {α : Type u} [linear_order α] :

An instance asserting that min a a = a

theorem min_lt_max {α : Type u} [linear_order α] {a b : α} :
a b
theorem max_lt_max {α : Type u} [linear_order α] {a b c d : α} (h₁ : a < c) (h₂ : b < d) :
theorem min_lt_min {α : Type u} [linear_order α] {a b c d : α} (h₁ : a < c) (h₂ : b < d) :
theorem min_right_comm {α : Type u} [linear_order α] (a b c : α) :
c = b
theorem max.left_comm {α : Type u} [linear_order α] (a b c : α) :
c) = c)
theorem max.right_comm {α : Type u} [linear_order α] (a b c : α) :
c = b
theorem monotone_on.map_max {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {s : set α} {a b : α} (hf : s) (ha : a s) (hb : b s) :
f b) = linear_order.max (f a) (f b)
theorem monotone_on.map_min {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {s : set α} {a b : α} (hf : s) (ha : a s) (hb : b s) :
f b) = linear_order.min (f a) (f b)
theorem antitone_on.map_max {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {s : set α} {a b : α} (hf : s) (ha : a s) (hb : b s) :
f b) = linear_order.min (f a) (f b)
theorem antitone_on.map_min {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {s : set α} {a b : α} (hf : s) (ha : a s) (hb : b s) :
f b) = linear_order.max (f a) (f b)
theorem monotone.map_max {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : monotone f) :
f b) = linear_order.max (f a) (f b)
theorem monotone.map_min {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : monotone f) :
f b) = linear_order.min (f a) (f b)
theorem antitone.map_max {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : antitone f) :
f b) = linear_order.min (f a) (f b)
theorem antitone.map_min {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : antitone f) :
f b) = linear_order.max (f a) (f b)
theorem min_choice {α : Type u} [linear_order α] (a b : α) :
= a = b
theorem max_choice {α : Type u} [linear_order α] (a b : α) :
= a = b
theorem le_of_max_le_left {α : Type u} [linear_order α] {a b c : α} (h : c) :
a c
theorem le_of_max_le_right {α : Type u} [linear_order α] {a b c : α} (h : c) :
b c
theorem max_commutative {α : Type u} [linear_order α] :
theorem max_associative {α : Type u} [linear_order α] :
theorem max_left_commutative {α : Type u} [linear_order α] :
theorem min_commutative {α : Type u} [linear_order α] :
theorem min_associative {α : Type u} [linear_order α] :
theorem min_left_commutative {α : Type u} [linear_order α] :