mathlib documentation

order.min_max

max and min #

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

Tags #

min, max

source
@[simp]
theorem le_min_iff {α : Type u} [linear_order α] {a b c : α} :
c ≤ min a b ↔ c ≤ a ∧ c ≤ b
source
@[simp]
theorem max_le_iff {α : Type u} [linear_order α] {a b c : α} :
max a b ≤ c ↔ a ≤ c ∧ b ≤ c
source
theorem max_le_max {α : Type u} [linear_order α] {a b c d : α} :
a ≤ c → b ≤ d → max a b ≤ max c d
source
theorem min_le_min {α : Type u} [linear_order α] {a b c d : α} :
a ≤ c → b ≤ d → min a b ≤ min c d
source
theorem le_max_of_le_left {α : Type u} [linear_order α] {a b c : α} :
a ≤ b → a ≤ max b c
source
theorem le_max_of_le_right {α : Type u} [linear_order α] {a b c : α} :
a ≤ c → a ≤ max b c
source
theorem lt_max_of_lt_left {α : Type u} [linear_order α] {a b c : α} (h : a < b) :
a < max b c
source
theorem lt_max_of_lt_right {α : Type u} [linear_order α] {a b c : α} (h : a < c) :
a < max b c
source
theorem min_le_of_left_le {α : Type u} [linear_order α] {a b c : α} :
a ≤ c → min a b ≤ c
source
theorem min_le_of_right_le {α : Type u} [linear_order α] {a b c : α} :
b ≤ c → min a b ≤ c
source
theorem min_lt_of_left_lt {α : Type u} [linear_order α] {a b c : α} (h : a < c) :
min a b < c
source
theorem min_lt_of_right_lt {α : Type u} [linear_order α] {a b c : α} (h : b < c) :
min a b < c
source
theorem max_min_distrib_left {α : Type u} [linear_order α] {a b c : α} :
max a (min b c) = min (max a b) (max a c)
source
theorem max_min_distrib_right {α : Type u} [linear_order α] {a b c : α} :
max (min a b) c = min (max a c) (max b c)
source
theorem min_max_distrib_left {α : Type u} [linear_order α] {a b c : α} :
min a (max b c) = max (min a b) (min a c)
source
theorem min_max_distrib_right {α : Type u} [linear_order α] {a b c : α} :
min (max a b) c = max (min a c) (min b c)
source
theorem min_le_max {α : Type u} [linear_order α] {a b : α} :
min a b ≤ max a b
source
@[simp]
theorem min_eq_left_iff {α : Type u} [linear_order α] {a b : α} :
min a b = a ↔ a ≤ b
source
@[simp]
theorem min_eq_right_iff {α : Type u} [linear_order α] {a b : α} :
min a b = b ↔ b ≤ a
source
@[simp]
theorem max_eq_left_iff {α : Type u} [linear_order α] {a b : α} :
max a b = a ↔ b ≤ a
source
@[simp]
theorem max_eq_right_iff {α : Type u} [linear_order α] {a b : α} :
max a b = b ↔ a ≤ b
source
theorem min_cases {α : Type u} [linear_order α] (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

source
theorem max_cases {α : Type u} [linear_order α] (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

source
theorem min_eq_iff {α : Type u} [linear_order α] {a b c : α} :
min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a
source
theorem max_eq_iff {α : Type u} [linear_order α] {a b c : α} :
max a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b
source
@[protected, instance]
def max_idem {α : Type u} [linear_order α] :
is_idempotent α max

An instance asserting that max a a = a

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

An instance asserting that min a a = a

source
@[simp]
theorem max_lt_iff {α : Type u} [linear_order α] {a b c : α} :
max a b < c ↔ a < c ∧ b < c
source
@[simp]
theorem lt_min_iff {α : Type u} [linear_order α] {a b c : α} :
a < min b c ↔ a < b ∧ a < c
source
@[simp]
theorem lt_max_iff {α : Type u} [linear_order α] {a b c : α} :
a < max b c ↔ a < b ∨ a < c
source
@[simp]
theorem min_lt_iff {α : Type u} [linear_order α] {a b c : α} :
min a b < c ↔ a < c ∨ b < c
source
@[simp]
theorem min_le_iff {α : Type u} [linear_order α] {a b c : α} :
min a b ≤ c ↔ a ≤ c ∨ b ≤ c
source
@[simp]
theorem le_max_iff {α : Type u} [linear_order α] {a b c : α} :
a ≤ max b c ↔ a ≤ b ∨ a ≤ c
source
theorem min_lt_max {α : Type u} [linear_order α] {a b : α} :
min a b < max a b ↔ a ≠ b
source
theorem max_lt_max {α : Type u} [linear_order α] {a b c d : α} (h₁ : a < c) (h₂ : b < d) :
max a b < max c d
source
theorem min_lt_min {α : Type u} [linear_order α] {a b c d : α} (h₁ : a < c) (h₂ : b < d) :
min a b < min c d
source
theorem min_right_comm {α : Type u} [linear_order α] (a b c : α) :
min (min a b) c = min (min a c) b
source
theorem max.left_comm {α : Type u} [linear_order α] (a b c : α) :
max a (max b c) = max b (max a c)
source
theorem max.right_comm {α : Type u} [linear_order α] (a b c : α) :
max (max a b) c = max (max a c) b
source
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 (max a b) = max (f a) (f b)
source
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 (min a b) = min (f a) (f b)
source
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 (max a b) = min (f a) (f b)
source
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 (min a b) = max (f a) (f b)
source
theorem monotone.map_max {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : monotone f) :
f (max a b) = max (f a) (f b)
source
theorem monotone.map_min {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : monotone f) :
f (min a b) = min (f a) (f b)
source
theorem antitone.map_max {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : antitone f) :
f (max a b) = min (f a) (f b)
source
theorem antitone.map_min {α : Type u} {β : Type v} [linear_order α] [linear_order β] {f : α → β} {a b : α} (hf : antitone f) :
f (min a b) = max (f a) (f b)
source
theorem min_rec {α : Type u} [linear_order α] {p : α → Prop} {x y : α} (hx : x ≤ y → p x) (hy : y ≤ x → p y) :
p (min x y)
source
theorem max_rec {α : Type u} [linear_order α] {p : α → Prop} {x y : α} (hx : y ≤ x → p x) (hy : x ≤ y → p y) :
p (max x y)
source
theorem min_rec' {α : Type u} [linear_order α] (p : α → Prop) {x y : α} (hx : p x) (hy : p y) :
p (min x y)
source
theorem max_rec' {α : Type u} [linear_order α] (p : α → Prop) {x y : α} (hx : p x) (hy : p y) :
p (max x y)
source
theorem min_choice {α : Type u} [linear_order α] (a b : α) :
min a b = a ∨ min a b = b
source
theorem max_choice {α : Type u} [linear_order α] (a b : α) :
max a b = a ∨ max a b = b
source
theorem le_of_max_le_left {α : Type u} [linear_order α] {a b c : α} (h : max a b ≤ c) :
a ≤ c
source
theorem le_of_max_le_right {α : Type u} [linear_order α] {a b c : α} (h : max a b ≤ c) :
b ≤ c
source
theorem max_commutative {α : Type u} [linear_order α] :
commutative max
source
theorem max_associative {α : Type u} [linear_order α] :
associative max
source
theorem max_left_commutative {α : Type u} [linear_order α] :
left_commutative max
source
theorem min_commutative {α : Type u} [linear_order α] :
commutative min
source
theorem min_associative {α : Type u} [linear_order α] :
associative min
source
theorem min_left_commutative {α : Type u} [linear_order α] :
left_commutative min