mathlib docs: core.init.algebra.functions

source

def min {α : Type u} [decidable_linear_order α] :

α → α → α

Equations

min a b = ite (a ≤ b) a b

source

def max {α : Type u} [decidable_linear_order α] :

α → α → α

Equations

max a b = ite (b ≤ a) a b

source

meta def tactic.interactive.min_tac :

interactive.parse (lean.parser.pexpr std.prec.max) → 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 : α} :

c ≤ a → 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 : α} :

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

source

theorem eq_min {α : Type u} [decidable_linear_order α] {a b c : α} :

c ≤ a → c ≤ b → (∀ {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 : α} :

a ≤ b → min a b = a

source

@[simp]

theorem min_eq_right {α : Type u} [decidable_linear_order α] {a b : α} :

b ≤ a → min a b = b

source

theorem eq_max {α : Type u} [decidable_linear_order α] {a b c : α} :

a ≤ c → b ≤ c → (∀ {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 : α} :

b ≤ a → max a b = a

source

@[simp]

theorem max_eq_right {α : Type u} [decidable_linear_order α] {a b : α} :

a ≤ b → max a b = b

source

theorem min_eq_left_of_lt {α : Type u} [decidable_linear_order α] {a b : α} :

a < b → min a b = a

source

theorem min_eq_right_of_lt {α : Type u} [decidable_linear_order α] {a b : α} :

b < a → min a b = b

source

theorem max_eq_left_of_lt {α : Type u} [decidable_linear_order α] {a b : α} :

b < a → max a b = a

source

theorem max_eq_right_of_lt {α : Type u} [decidable_linear_order α] {a b : α} :

a < b → max a b = b

source

theorem lt_min {α : Type u} [decidable_linear_order α] {a b c : α} :

a < b → a < c → a < min b c

source

theorem max_lt {α : Type u} [decidable_linear_order α] {a b c : α} :

a < c → b < c → max a b < c

mathlib documentation

core.init.algebra.functions

General documentation

Additional documentation

Library

mathlib documentation

core.​init.​algebra.​functions

General documentation

Additional documentation

Library

core.init.algebra.functions