Basic lemmas about linear orders.

The contents of this file came from init.algebra.functions in Lean 3, and it would be good to find everything a better home.

theorem min_def {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b = if a ≤ b then a else b

theorem max_def {α : Type u} [LinearOrder α] (a : α) (b : α) : max a b = if a ≤ b then b else a

theorem min_le_left {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b ≤ a

theorem min_le_right {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b ≤ b

theorem le_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b

theorem le_max_left {α : Type u} [LinearOrder α] (a : α) (b : α) : a ≤ max a b

theorem le_max_right {α : Type u} [LinearOrder α] (a : α) (b : α) : b ≤ max a b

theorem max_le {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) : max a b ≤ c

theorem eq_min {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : c ≤ a) (h₂ : c ≤ b) (h₃ : ∀ {d : α}, d ≤ a → d ≤ b → d ≤ c) : c = min a b

theorem min_comm {α : Type u} [LinearOrder α] (a : α) (b : α) : min a b = min b a

theorem min_assoc {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : min (min a b) c = min a (min b c)

theorem min_left_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : min a (min b c) = min b (min a c)

@[simp]

theorem min_self {α : Type u} [LinearOrder α] (a : α) : min a a = a

theorem min_eq_left {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) : min a b = a

theorem min_eq_right {α : Type u} [LinearOrder α] {a : α} {b : α} (h : b ≤ a) : min a b = b

theorem eq_max {α : Type u} [LinearOrder α] {a : α} {b : α} {c : α} (h₁ : a ≤ c) (h₂ : b ≤ c) (h₃ : ∀ {d : α}, a ≤ d → b ≤ d → c ≤ d) : c = max a b

theorem max_comm {α : Type u} [LinearOrder α] (a : α) (b : α) : max a b = max b a

theorem max_assoc {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : max (max a b) c = max a (max b c)

theorem max_left_comm {α : Type u} [LinearOrder α] (a : α) (b : α) (c : α) : max a (max b c) = max b (max a c)

@[simp]

theorem max_self {α : Type u} [LinearOrder α] (a : α) : max a a = a

theorem max_eq_left {α : Type u} [LinearOrder α] {a : α} {b : α} (h : b ≤ a) : max a b = a

theorem max_eq_right {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a ≤ b) : max a b = b

theorem min_eq_left_of_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : a < b) : min a b = a

theorem min_eq_right_of_lt {α : Type u} [LinearOrder α] {a : α} {b : α} (h : b < a) : min a b = b

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

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

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

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