mathlib documentation

core.init.algebra.functions

source
def min {α : Type u} [decidable_linear_order α] (a b : α) :
α

Equations
source
def max {α : Type u} [decidable_linear_order α] (a b : α) :
α

Equations
source
meta def tactic.interactive.min_tac (a b : interactive.parse (lean.parser.pexpr std.prec.max)) :
tactic unit

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

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

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

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

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

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

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

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

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

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

source
@[simp]
theorem min_self {α : Type u} [decidable_linear_order α] (a : α) :
min a a = a

source
@[simp]
theorem min_eq_left {α : Type u} [decidable_linear_order α] {a b : α} (h : a ≤ b) :
min a b = a

source
@[simp]
theorem min_eq_right {α : Type u} [decidable_linear_order α] {a b : α} (h : b ≤ a) :
min a b = b

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

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

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

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

source
@[simp]
theorem max_self {α : Type u} [decidable_linear_order α] (a : α) :
max a a = a

source
@[simp]
theorem max_eq_left {α : Type u} [decidable_linear_order α] {a b : α} (h : b ≤ a) :
max a b = a

source
@[simp]
theorem max_eq_right {α : Type u} [decidable_linear_order α] {a b : α} (h : a ≤ b) :
max a b = b

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

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

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

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

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

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