Documentation

Mathlib.Algebra.Order.Monoid.MinMax

Lemmas about min and max in an ordered monoid. #

Some lemmas about types that have an ordering and a binary operation, with no rules relating them.

source
ink
theorem fn_min_add_fn_max {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : AddCommSemigroup β] (f : α → β) (n : α) (m : α) :
f (min n m) + f (max n m) = f n + f m
source
ink
theorem fn_min_mul_fn_max {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst : CommSemigroup β] (f : α → β) (n : α) (m : α) :
f (min n m) * f (max n m) = f n * f m
source
ink
theorem min_add_max {α : Type u_1} [inst : LinearOrder α] [inst : AddCommSemigroup α] (n : α) (m : α) :
min n m + max n m = n + m
source
ink
theorem min_mul_max {α : Type u_1} [inst : LinearOrder α] [inst : CommSemigroup α] (n : α) (m : α) :
min n m * max n m = n * m
source
ink
theorem min_add_add_left {α : Type u_1} [inst : LinearOrder α] [inst : Add α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
min (a + b) (a + c) = a + min b c
source
ink
theorem min_mul_mul_left {α : Type u_1} [inst : LinearOrder α] [inst : Mul α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
min (a * b) (a * c) = a * min b c
source
ink
theorem max_add_add_left {α : Type u_1} [inst : LinearOrder α] [inst : Add α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
max (a + b) (a + c) = a + max b c
source
ink
theorem max_mul_mul_left {α : Type u_1} [inst : LinearOrder α] [inst : Mul α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
max (a * b) (a * c) = a * max b c
source
ink
theorem lt_or_lt_of_add_lt_add {α : Type u_1} [inst : LinearOrder α] [inst : Add α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {m : α} {n : α} (h : m + n < a + b) :
m < a ∨ n < b
source
ink
theorem lt_or_lt_of_mul_lt_mul {α : Type u_1} [inst : LinearOrder α] [inst : Mul α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {m : α} {n : α} (h : m * n < a * b) :
m < a ∨ n < b
source
ink
theorem add_lt_add_iff_of_le_of_le {α : Type u_1} [inst : LinearOrder α] [inst : Add α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (ac : a ≤ c) (bd : b ≤ d) :
a + b < c + d ↔ a < c ∨ b < d
source
ink
theorem mul_lt_mul_iff_of_le_of_le {α : Type u_1} [inst : LinearOrder α] [inst : Mul α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} {c : α} {d : α} (ac : a ≤ c) (bd : b ≤ d) :
a * b < c * d ↔ a < c ∨ b < d
source
ink
theorem min_add_add_right {α : Type u_1} [inst : LinearOrder α] [inst : Add α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
min (a + c) (b + c) = min a b + c
source
ink
theorem min_mul_mul_right {α : Type u_1} [inst : LinearOrder α] [inst : Mul α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
min (a * c) (b * c) = min a b * c
source
ink
theorem max_add_add_right {α : Type u_1} [inst : LinearOrder α] [inst : Add α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
max (a + c) (b + c) = max a b + c
source
ink
theorem max_mul_mul_right {α : Type u_1} [inst : LinearOrder α] [inst : Mul α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) (b : α) (c : α) :
max (a * c) (b * c) = max a b * c
source
ink
theorem min_le_add_of_nonneg_right {α : Type u_1} [inst : LinearOrder α] [inst : AddZeroClass α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (hb : 0 ≤ b) :
min a b ≤ a + b
source
ink
theorem min_le_mul_of_one_le_right {α : Type u_1} [inst : LinearOrder α] [inst : MulOneClass α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (hb : 1 ≤ b) :
min a b ≤ a * b
source
ink
theorem min_le_add_of_nonneg_left {α : Type u_1} [inst : LinearOrder α] [inst : AddZeroClass α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) :
min a b ≤ a + b
source
ink
theorem min_le_mul_of_one_le_left {α : Type u_1} [inst : LinearOrder α] [inst : MulOneClass α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) :
min a b ≤ a * b
source
ink
theorem max_le_add_of_nonneg {α : Type u_1} [inst : LinearOrder α] [inst : AddZeroClass α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
max a b ≤ a + b
source
ink
theorem max_le_mul_of_one_le {α : Type u_1} [inst : LinearOrder α] [inst : MulOneClass α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
max a b ≤ a * b