`max` and `min` #

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

Tags #

min, max

source

@[simp]

theorem le_min_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

c ≤ min a b ↔ c ≤ a ∧ c ≤ b

source

@[simp]

theorem le_max_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

a ≤ max b c ↔ a ≤ b ∨ a ≤ c

source

@[simp]

theorem min_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

min a b ≤ c ↔ a ≤ c ∨ b ≤ c

source

@[simp]

theorem max_le_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

max a b ≤ c ↔ a ≤ c ∧ b ≤ c

source

@[simp]

theorem lt_min_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

a < min b c ↔ a < b ∧ a < c

source

@[simp]

theorem lt_max_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

a < max b c ↔ a < b ∨ a < c

source

@[simp]

theorem min_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

min a b < c ↔ a < c ∨ b < c

source

@[simp]

theorem max_lt_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

max a b < c ↔ a < c ∧ b < c

source

theorem max_le_max {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} :

a ≤ c → b ≤ d → max a b ≤ max c d

source

theorem max_le_max_left {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) :

max c a ≤ max c b

source

theorem max_le_max_right {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) :

max a c ≤ max b c

source

theorem min_le_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} :

a ≤ c → b ≤ d → min a b ≤ min c d

source

theorem min_le_min_left {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) :

min c a ≤ min c b

source

theorem min_le_min_right {α : Type u} [LinearOrder α] {a : α} {b : α} (c : α) (h : a ≤ b) :

min a c ≤ min b c

source

theorem le_max_of_le_left {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

a ≤ b → a ≤ max b c

source

theorem le_max_of_le_right {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

a ≤ c → a ≤ max b c

source

theorem lt_max_of_lt_left {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a < b) :

a < max b c

source

theorem lt_max_of_lt_right {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a < c) :

a < max b c

source

theorem min_le_of_left_le {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

a ≤ c → min a b ≤ c

source

theorem min_le_of_right_le {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

b ≤ c → min a b ≤ c

source

theorem min_lt_of_left_lt {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : a < c) :

min a b < c

source

theorem min_lt_of_right_lt {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h : b < c) :

min a b < c

source

theorem max_min_distrib_left {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) :

max a (min b c) = min (max a b) (max a c)

source

theorem max_min_distrib_right {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) :

max (min a b) c = min (max a c) (max b c)

source

theorem min_max_distrib_left {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) :

min a (max b c) = max (min a b) (min a c)

source

theorem min_max_distrib_right {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) :

min (max a b) c = max (min a c) (min b c)

source

theorem min_le_max {α : Type u} [LinearOrder α] {a : α} {b : α} :

min a b ≤ max a b

source

@[simp]

theorem min_eq_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} :

min a b = a ↔ a ≤ b

source

@[simp]

theorem min_eq_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} :

min a b = b ↔ b ≤ a

source

@[simp]

theorem max_eq_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} :

max a b = a ↔ b ≤ a

source

@[simp]

theorem max_eq_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} :

max a b = b ↔ a ≤ b

source

theorem min_cases {α : Type u} [LinearOrder α] (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} [LinearOrder α] (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} [LinearOrder α] {a : α} {b : α} {c : α} :

min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a

source

theorem max_eq_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

max a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b

source

theorem min_lt_min_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

min a c < min b c ↔ a < b ∧ a < c

source

theorem min_lt_min_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

min a b < min a c ↔ b < c ∧ b < a

source

theorem max_lt_max_left_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

max a c < max b c ↔ a < b ∧ c < b

source

theorem max_lt_max_right_iff {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} :

max a b < max a c ↔ b < c ∧ a < c

source

instance max_idem {α : Type u} [LinearOrder α] :

Std.IdempotentOp max

An instance asserting that max a a = a

Equations

⋯ = ⋯

source

instance min_idem {α : Type u} [LinearOrder α] :

Std.IdempotentOp min

An instance asserting that min a a = a

Equations

⋯ = ⋯

source

theorem min_lt_max {α : Type u} [LinearOrder α] {a : α} {b : α} :

min a b < max a b ↔ a ≠ b

source

theorem max_lt_max {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < c) (h₂ : b < d) :

max a b < max c d

source

theorem min_lt_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} {d : α} (h₁ : a < c) (h₂ : b < d) :

min a b < min c d

source

theorem min_right_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) :

min (min a b) c = min (min a c) b

source

theorem Max.left_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) :

max a (max b c) = max b (max a c)

source

theorem Max.right_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) :

max (max a b) c = max (max a c) b

source

theorem MonotoneOn.map_max {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) :

f (max a b) = max (f a) (f b)

source

theorem MonotoneOn.map_min {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) :

f (min a b) = min (f a) (f b)

source

theorem AntitoneOn.map_max {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) :

f (max a b) = min (f a) (f b)

source

theorem AntitoneOn.map_min {α : Type u} {β : Type v} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Set α} {a : α} {b : α} (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) :