mathlib3 documentation

theorem min_def {α : Type u} [linear_order α] (a b : α) :

theorem max_def {α : Type u} [linear_order α] (a b : α) :

theorem min_le_left {α : Type u} [linear_order α] (a b : α) :

theorem min_le_right {α : Type u} [linear_order α] (a b : α) :

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

theorem le_max_left {α : Type u} [linear_order α] (a b : α) :

theorem le_max_right {α : Type u} [linear_order α] (a b : α) :

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

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

theorem min_comm {α : Type u} [linear_order α] (a b : α) :

theorem min_assoc {α : Type u} [linear_order α] (a b c : α) :

theorem min_left_comm {α : Type u} [linear_order α] (a b c : α) :

theorem min_self {α : Type u} [linear_order α] (a : α) :

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

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

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

theorem max_comm {α : Type u} [linear_order α] (a b : α) :

theorem max_assoc {α : Type u} [linear_order α] (a b c : α) :

theorem max_left_comm {α : Type u} [linear_order α] (a b c : α) :

theorem max_self {α : Type u} [linear_order α] (a : α) :

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

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

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

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

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

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

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

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