Documentation

Mathlib.Algebra.Order.Monoid.Unbundled.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.

theorem fn_min_mul_fn_max {α : Type u_1} {β : Type u_2} [LinearOrder α] [CommSemigroup β] (f : αβ) (a : α) (b : α) :
f (a b) * f (a b) = f a * f b
theorem fn_min_add_fn_max {α : Type u_1} {β : Type u_2} [LinearOrder α] [AddCommSemigroup β] (f : αβ) (a : α) (b : α) :
f (a b) + f (a b) = f a + f b
theorem fn_max_mul_fn_min {α : Type u_1} {β : Type u_2} [LinearOrder α] [CommSemigroup β] (f : αβ) (a : α) (b : α) :
f (a b) * f (a b) = f a * f b
theorem fn_max_add_fn_min {α : Type u_1} {β : Type u_2} [LinearOrder α] [AddCommSemigroup β] (f : αβ) (a : α) (b : α) :
f (a b) + f (a b) = f a + f b
@[simp]
theorem min_mul_max {α : Type u_1} [LinearOrder α] [CommSemigroup α] (a : α) (b : α) :
(a b) * (a b) = a * b
@[simp]
theorem min_add_max {α : Type u_1} [LinearOrder α] [AddCommSemigroup α] (a : α) (b : α) :
a b + a b = a + b
@[simp]
theorem max_mul_min {α : Type u_1} [LinearOrder α] [CommSemigroup α] (a : α) (b : α) :
(a b) * (a b) = a * b
@[simp]
theorem max_add_min {α : Type u_1} [LinearOrder α] [AddCommSemigroup α] (a : α) (b : α) :
a b + a b = a + b
theorem min_mul_mul_left {α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] (a : α) (b : α) (c : α) :
a * b a * c = a * (b c)
theorem min_add_add_left {α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] (a : α) (b : α) (c : α) :
(a + b) (a + c) = a + b c
theorem max_mul_mul_left {α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] (a : α) (b : α) (c : α) :
a * b a * c = a * (b c)
theorem max_add_add_left {α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] (a : α) (b : α) (c : α) :
(a + b) (a + c) = a + b c
theorem min_mul_mul_right {α : Type u_1} [LinearOrder α] [Mul α] [MulRightMono α] (a : α) (b : α) (c : α) :
a * c b * c = (a b) * c
theorem min_add_add_right {α : Type u_1} [LinearOrder α] [Add α] [AddRightMono α] (a : α) (b : α) (c : α) :
(a + c) (b + c) = a b + c
theorem max_mul_mul_right {α : Type u_1} [LinearOrder α] [Mul α] [MulRightMono α] (a : α) (b : α) (c : α) :
a * c b * c = (a b) * c
theorem max_add_add_right {α : Type u_1} [LinearOrder α] [Add α] [AddRightMono α] (a : α) (b : α) (c : α) :
(a + c) (b + c) = a b + c
theorem lt_or_lt_of_mul_lt_mul {α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] [MulRightMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ * b₁ < a₂ * b₂a₁ < a₂ b₁ < b₂
theorem lt_or_lt_of_add_lt_add {α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] [AddRightMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ + b₁ < a₂ + b₂a₁ < a₂ b₁ < b₂
theorem le_or_lt_of_mul_le_mul {α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] [MulRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ * b₁ a₂ * b₂a₁ a₂ b₁ < b₂
theorem le_or_lt_of_add_le_add {α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] [AddRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ + b₁ a₂ + b₂a₁ a₂ b₁ < b₂
theorem lt_or_le_of_mul_le_mul {α : Type u_1} [LinearOrder α] [Mul α] [MulLeftStrictMono α] [MulRightMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ * b₁ a₂ * b₂a₁ < a₂ b₁ b₂
theorem lt_or_le_of_add_le_add {α : Type u_1} [LinearOrder α] [Add α] [AddLeftStrictMono α] [AddRightMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ + b₁ a₂ + b₂a₁ < a₂ b₁ b₂
theorem le_or_le_of_mul_le_mul {α : Type u_1} [LinearOrder α] [Mul α] [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ * b₁ a₂ * b₂a₁ a₂ b₁ b₂
theorem le_or_le_of_add_le_add {α : Type u_1} [LinearOrder α] [Add α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} :
a₁ + b₁ a₂ + b₂a₁ a₂ b₁ b₂
theorem mul_lt_mul_iff_of_le_of_le {α : Type u_1} [LinearOrder α] [Mul α] [MulLeftMono α] [MulRightMono α] [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ a₂) (hb : b₁ b₂) :
a₁ * b₁ < a₂ * b₂ a₁ < a₂ b₁ < b₂
theorem add_lt_add_iff_of_le_of_le {α : Type u_1} [LinearOrder α] [Add α] [AddLeftMono α] [AddRightMono α] [AddLeftStrictMono α] [AddRightStrictMono α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ a₂) (hb : b₁ b₂) :
a₁ + b₁ < a₂ + b₂ a₁ < a₂ b₁ < b₂
theorem min_le_mul_of_one_le_right {α : Type u_1} [LinearOrder α] [MulOneClass α] [MulLeftMono α] {a : α} {b : α} (hb : 1 b) :
a b a * b
theorem min_le_add_of_nonneg_right {α : Type u_1} [LinearOrder α] [AddZeroClass α] [AddLeftMono α] {a : α} {b : α} (hb : 0 b) :
a b a + b
theorem min_le_mul_of_one_le_left {α : Type u_1} [LinearOrder α] [MulOneClass α] [MulRightMono α] {a : α} {b : α} (ha : 1 a) :
a b a * b
theorem min_le_add_of_nonneg_left {α : Type u_1} [LinearOrder α] [AddZeroClass α] [AddRightMono α] {a : α} {b : α} (ha : 0 a) :
a b a + b
theorem max_le_mul_of_one_le {α : Type u_1} [LinearOrder α] [MulOneClass α] [MulLeftMono α] [MulRightMono α] {a : α} {b : α} (ha : 1 a) (hb : 1 b) :
a b a * b
theorem max_le_add_of_nonneg {α : Type u_1} [LinearOrder α] [AddZeroClass α] [AddLeftMono α] [AddRightMono α] {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
a b a + b