max
and min
#
This file proves basic properties about maxima and minima on a linear_order
.
Tags #
min, max
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
max_le_max
{α : Type u}
[linear_order α]
{a b c d : α} :
a ≤ c → b ≤ d → linear_order.max a b ≤ linear_order.max c d
theorem
min_le_min
{α : Type u}
[linear_order α]
{a b c d : α} :
a ≤ c → b ≤ d → linear_order.min a b ≤ linear_order.min c d
theorem
le_max_of_le_left
{α : Type u}
[linear_order α]
{a b c : α} :
a ≤ b → a ≤ linear_order.max b c
theorem
le_max_of_le_right
{α : Type u}
[linear_order α]
{a b c : α} :
a ≤ c → a ≤ linear_order.max b c
theorem
lt_max_of_lt_left
{α : Type u}
[linear_order α]
{a b c : α}
(h : a < b) :
a < linear_order.max b c
theorem
lt_max_of_lt_right
{α : Type u}
[linear_order α]
{a b c : α}
(h : a < c) :
a < linear_order.max b c
theorem
min_le_of_left_le
{α : Type u}
[linear_order α]
{a b c : α} :
a ≤ c → linear_order.min a b ≤ c
theorem
min_le_of_right_le
{α : Type u}
[linear_order α]
{a b c : α} :
b ≤ c → linear_order.min a b ≤ c
theorem
min_lt_of_left_lt
{α : Type u}
[linear_order α]
{a b c : α}
(h : a < c) :
linear_order.min a b < c
theorem
min_lt_of_right_lt
{α : Type u}
[linear_order α]
{a b c : α}
(h : b < c) :
linear_order.min a b < c
theorem
max_min_distrib_left
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.max a (linear_order.min b c) = linear_order.min (linear_order.max a b) (linear_order.max a c)
theorem
max_min_distrib_right
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.max (linear_order.min a b) c = linear_order.min (linear_order.max a c) (linear_order.max b c)
theorem
min_max_distrib_left
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.min a (linear_order.max b c) = linear_order.max (linear_order.min a b) (linear_order.min a c)
theorem
min_max_distrib_right
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.min (linear_order.max a b) c = linear_order.max (linear_order.min a c) (linear_order.min b c)
theorem
min_le_max
{α : Type u}
[linear_order α]
{a b : α} :
linear_order.min a b ≤ linear_order.max a b
@[simp]
@[simp]
@[simp]
@[simp]
theorem
min_cases
{α : Type u}
[linear_order α]
(a b : α) :
linear_order.min a b = a ∧ a ≤ b ∨ linear_order.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}
[linear_order α]
(a b : α) :
linear_order.max a b = a ∧ b ≤ a ∨ linear_order.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_lt_min_left_iff
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.min a c < linear_order.min b c ↔ a < b ∧ a < c
theorem
min_lt_min_right_iff
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.min a b < linear_order.min a c ↔ b < c ∧ b < a
theorem
max_lt_max_left_iff
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.max a c < linear_order.max b c ↔ a < b ∧ c < b
theorem
max_lt_max_right_iff
{α : Type u}
[linear_order α]
{a b c : α} :
linear_order.max a b < linear_order.max a c ↔ b < c ∧ a < c
@[protected, instance]
An instance asserting that max a a = a
@[protected, instance]
An instance asserting that min a a = a
theorem
min_lt_max
{α : Type u}
[linear_order α]
{a b : α} :
linear_order.min a b < linear_order.max a b ↔ a ≠ b
theorem
max_lt_max
{α : Type u}
[linear_order α]
{a b c d : α}
(h₁ : a < c)
(h₂ : b < d) :
linear_order.max a b < linear_order.max c d
theorem
min_lt_min
{α : Type u}
[linear_order α]
{a b c d : α}
(h₁ : a < c)
(h₂ : b < d) :
linear_order.min a b < linear_order.min c d
theorem
min_right_comm
{α : Type u}
[linear_order α]
(a b c : α) :
linear_order.min (linear_order.min a b) c = linear_order.min (linear_order.min a c) b
theorem
max.left_comm
{α : Type u}
[linear_order α]
(a b c : α) :
linear_order.max a (linear_order.max b c) = linear_order.max b (linear_order.max a c)
theorem
max.right_comm
{α : Type u}
[linear_order α]
(a b c : α) :
linear_order.max (linear_order.max a b) c = linear_order.max (linear_order.max a c) b
theorem
monotone_on.map_max
{α : Type u}
{β : Type v}
[linear_order α]
[linear_order β]
{f : α → β}
{s : set α}
{a b : α}
(hf : monotone_on f s)
(ha : a ∈ s)
(hb : b ∈ s) :
f (linear_order.max a 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 : monotone_on f s)
(ha : a ∈ s)
(hb : b ∈ s) :
f (linear_order.min a 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 : antitone_on f s)
(ha : a ∈ s)
(hb : b ∈ s) :
f (linear_order.max a 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 : antitone_on f s)
(ha : a ∈ s)
(hb : b ∈ s) :
f (linear_order.min a 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 (linear_order.max a 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 (linear_order.min a 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 (linear_order.max a 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 (linear_order.min a b) = linear_order.max (f a) (f b)
theorem
min_choice
{α : Type u}
[linear_order α]
(a b : α) :
linear_order.min a b = a ∨ linear_order.min a b = b
theorem
max_choice
{α : Type u}
[linear_order α]
(a b : α) :
linear_order.max a b = a ∨ linear_order.max a b = b
theorem
le_of_max_le_left
{α : Type u}
[linear_order α]
{a b c : α}
(h : linear_order.max a b ≤ c) :
a ≤ c
theorem
le_of_max_le_right
{α : Type u}
[linear_order α]
{a b c : α}
(h : linear_order.max a b ≤ c) :
b ≤ c