# mathlibdocumentation

core / init.algebra.functions

theorem min_def {α : Type u} [linear_order α] (a b : α) :
= ite (a b) a b
theorem max_def {α : Type u} [linear_order α] (a b : α) :
= ite (b a) a b
theorem min_le_left {α : Type u} [linear_order α] (a b : α) :
a
theorem min_le_right {α : Type u} [linear_order α] (a b : α) :
b
theorem le_min {α : Type u} [linear_order α] {a b c : α} (h₁ : c a) (h₂ : c b) :
c
theorem le_max_left {α : Type u} [linear_order α] (a b : α) :
a
theorem le_max_right {α : Type u} [linear_order α] (a b : α) :
b
theorem max_le {α : Type u} [linear_order α] {a b c : α} (h₁ : a c) (h₂ : b c) :
c
theorem eq_min {α : Type u} [linear_order α] {a b c : α} (h₁ : c a) (h₂ : c b) (h₃ : ∀ {d : α}, d ad bd c) :
c =
theorem min_comm {α : Type u} [linear_order α] (a b : α) :
theorem min_assoc {α : Type u} [linear_order α] (a b c : α) :
c = c)
theorem min_left_comm {α : Type u} [linear_order α] (a b c : α) :
c) = c)
@[simp]
theorem min_self {α : Type u} [linear_order α] (a : α) :
= a
@[simp]
theorem min_eq_left {α : Type u} [linear_order α] {a b : α} (h : a b) :
= a
@[simp]
theorem min_eq_right {α : Type u} [linear_order α] {a b : α} (h : b a) :
= b
theorem eq_max {α : Type u} [linear_order α] {a b c : α} (h₁ : a c) (h₂ : b c) (h₃ : ∀ {d : α}, a db dc d) :
c =
theorem max_comm {α : Type u} [linear_order α] (a b : α) :
theorem max_assoc {α : Type u} [linear_order α] (a b c : α) :
c = c)
theorem max_left_comm {α : Type u} [linear_order α] (a b c : α) :
c) = c)
@[simp]
theorem max_self {α : Type u} [linear_order α] (a : α) :
= a
@[simp]
theorem max_eq_left {α : Type u} [linear_order α] {a b : α} (h : b a) :
= a
@[simp]
theorem max_eq_right {α : Type u} [linear_order α] {a b : α} (h : a b) :
= b
theorem min_eq_left_of_lt {α : Type u} [linear_order α] {a b : α} (h : a < b) :
= a
theorem min_eq_right_of_lt {α : Type u} [linear_order α] {a b : α} (h : b < a) :
= b
theorem max_eq_left_of_lt {α : Type u} [linear_order α] {a b : α} (h : b < a) :
= a
theorem max_eq_right_of_lt {α : Type u} [linear_order α] {a b : α} (h : a < b) :
= b
theorem lt_min {α : Type u} [linear_order α] {a b c : α} (h₁ : a < b) (h₂ : a < c) :
a <
theorem max_lt {α : Type u} [linear_order α] {a b c : α} (h₁ : a < c) (h₂ : b < c) :
< c