mathlib3documentation

algebra.order.monoid.min_max

Lemmas about min and max in an ordered monoid. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [linear_order α] (f : α β) (n m : α) :
f m) * f m) = f n * f m
theorem fn_min_add_fn_max {α : Type u_1} {β : Type u_2} [linear_order α] (f : α β) (n m : α) :
f m) + f m) = f n + f m
theorem min_add_max {α : Type u_1} [linear_order α] (n m : α) :
= n + m
theorem min_mul_max {α : Type u_1} [linear_order α] (n m : α) :
= n * m
theorem min_mul_mul_left {α : Type u_1} [linear_order α] [has_mul α] (a b c : α) :
linear_order.min (a * b) (a * c) = a *
linear_order.min (a + b) (a + c) = a +
linear_order.max (a + b) (a + c) = a +
theorem max_mul_mul_left {α : Type u_1} [linear_order α] [has_mul α] (a b c : α) :
linear_order.max (a * b) (a * c) = a *
linear_order.min (a + c) (b + c) = + c
theorem min_mul_mul_right {α : Type u_1} [linear_order α] [has_mul α] (a b c : α) :
linear_order.min (a * c) (b * c) = * c
theorem max_mul_mul_right {α : Type u_1} [linear_order α] [has_mul α] (a b c : α) :
linear_order.max (a * c) (b * c) = * c
linear_order.max (a + c) (b + c) = + c
theorem lt_or_lt_of_add_lt_add {α : Type u_1} [linear_order α] [has_add α] {a₁ a₂ b₁ b₂ : α} :
a₁ + b₁ < a₂ + b₂ a₁ < a₂ b₁ < b₂
theorem lt_or_lt_of_mul_lt_mul {α : Type u_1} [linear_order α] [has_mul α] {a₁ a₂ b₁ b₂ : α} :
a₁ * b₁ < a₂ * b₂ a₁ < a₂ b₁ < b₂
theorem le_or_lt_of_mul_le_mul {α : Type u_1} [linear_order α] [has_mul α] {a₁ a₂ b₁ b₂ : α} :
a₁ * b₁ a₂ * b₂ a₁ a₂ b₁ < b₂
theorem le_or_lt_of_add_le_add {α : Type u_1} [linear_order α] [has_add α] {a₁ a₂ b₁ b₂ : α} :
a₁ + b₁ a₂ + b₂ a₁ a₂ b₁ < b₂
theorem lt_or_le_of_add_le_add {α : Type u_1} [linear_order α] [has_add α] {a₁ a₂ b₁ b₂ : α} :
a₁ + b₁ a₂ + b₂ a₁ < a₂ b₁ b₂
theorem lt_or_le_of_mul_le_mul {α : Type u_1} [linear_order α] [has_mul α] {a₁ a₂ b₁ b₂ : α} :
a₁ * b₁ a₂ * b₂ a₁ < a₂ b₁ b₂
theorem le_or_le_of_mul_le_mul {α : Type u_1} [linear_order α] [has_mul α] {a₁ a₂ b₁ b₂ : α} :
a₁ * b₁ a₂ * b₂ a₁ a₂ b₁ b₂
theorem le_or_le_of_add_le_add {α : Type u_1} [linear_order α] [has_add α] {a₁ a₂ b₁ b₂ : α} :
a₁ + b₁ a₂ + b₂ a₁ a₂ b₁ b₂
theorem mul_lt_mul_iff_of_le_of_le {α : Type u_1} [linear_order α] [has_mul α] {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} [linear_order α] [has_add α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ a₂) (hb : b₁ b₂) :
a₁ + b₁ < a₂ + b₂ a₁ < a₂ b₁ < b₂
theorem min_le_add_of_nonneg_right {α : Type u_1} [linear_order α] {a b : α} (hb : 0 b) :
a + b
theorem min_le_mul_of_one_le_right {α : Type u_1} [linear_order α] {a b : α} (hb : 1 b) :
a * b
theorem min_le_add_of_nonneg_left {α : Type u_1} [linear_order α] {a b : α} (ha : 0 a) :
a + b
theorem min_le_mul_of_one_le_left {α : Type u_1} [linear_order α] {a b : α} (ha : 1 a) :
a * b
theorem max_le_mul_of_one_le {α : Type u_1} [linear_order α] {a b : α} (ha : 1 a) (hb : 1 b) :
a * b
theorem max_le_add_of_nonneg {α : Type u_1} [linear_order α] {a b : α} (ha : 0 a) (hb : 0 b) :
a + b