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 α]
[comm_semigroup β]
(f : α → β)
(n m : α) :
f (linear_order.min n m) * f (linear_order.max n m) = f n * f m
theorem
fn_min_add_fn_max
{α : Type u_1}
{β : Type u_2}
[linear_order α]
[add_comm_semigroup β]
(f : α → β)
(n m : α) :
f (linear_order.min n m) + f (linear_order.max n m) = f n + f m
theorem
min_add_max
{α : Type u_1}
[linear_order α]
[add_comm_semigroup α]
(n m : α) :
linear_order.min n m + linear_order.max n m = n + m
theorem
min_mul_max
{α : Type u_1}
[linear_order α]
[comm_semigroup α]
(n m : α) :
linear_order.min n m * linear_order.max n m = n * m
theorem
min_mul_mul_left
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
(a b c : α) :
linear_order.min (a * b) (a * c) = a * linear_order.min b c
theorem
min_add_add_left
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
(a b c : α) :
linear_order.min (a + b) (a + c) = a + linear_order.min b c
theorem
max_add_add_left
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
(a b c : α) :
linear_order.max (a + b) (a + c) = a + linear_order.max b c
theorem
max_mul_mul_left
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
(a b c : α) :
linear_order.max (a * b) (a * c) = a * linear_order.max b c
theorem
min_add_add_right
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a b c : α) :
linear_order.min (a + c) (b + c) = linear_order.min a b + c
theorem
min_mul_mul_right
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a b c : α) :
linear_order.min (a * c) (b * c) = linear_order.min a b * c
theorem
max_mul_mul_right
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a b c : α) :
linear_order.max (a * c) (b * c) = linear_order.max a b * c
theorem
max_add_add_right
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a b c : α) :
linear_order.max (a + c) (b + c) = linear_order.max a b + c
theorem
lt_or_lt_of_add_lt_add
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a₁ a₂ b₁ b₂ : α} :
theorem
lt_or_lt_of_mul_lt_mul
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a₁ a₂ b₁ b₂ : α} :
theorem
le_or_lt_of_mul_le_mul
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a₁ a₂ b₁ b₂ : α} :
theorem
le_or_lt_of_add_le_add
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a₁ a₂ b₁ b₂ : α} :
theorem
lt_or_le_of_add_le_add
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a₁ a₂ b₁ b₂ : α} :
theorem
lt_or_le_of_mul_le_mul
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a₁ a₂ b₁ b₂ : α} :
theorem
le_or_le_of_mul_le_mul
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a₁ a₂ b₁ b₂ : α} :
theorem
le_or_le_of_add_le_add
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a₁ a₂ b₁ b₂ : α} :
theorem
mul_lt_mul_iff_of_le_of_le
{α : Type u_1}
[linear_order α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
[covariant_class α α has_mul.mul has_lt.lt]
[covariant_class α α (function.swap has_mul.mul) has_lt.lt]
{a₁ a₂ b₁ b₂ : α}
(ha : a₁ ≤ a₂)
(hb : b₁ ≤ b₂) :
theorem
add_lt_add_iff_of_le_of_le
{α : Type u_1}
[linear_order α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_lt.lt]
{a₁ a₂ b₁ b₂ : α}
(ha : a₁ ≤ a₂)
(hb : b₁ ≤ b₂) :
theorem
min_le_add_of_nonneg_right
{α : Type u_1}
[linear_order α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
{a b : α}
(hb : 0 ≤ b) :
linear_order.min a b ≤ a + b
theorem
min_le_mul_of_one_le_right
{α : Type u_1}
[linear_order α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
{a b : α}
(hb : 1 ≤ b) :
linear_order.min a b ≤ a * b
theorem
min_le_add_of_nonneg_left
{α : Type u_1}
[linear_order α]
[add_zero_class α]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : 0 ≤ a) :
linear_order.min a b ≤ a + b
theorem
min_le_mul_of_one_le_left
{α : Type u_1}
[linear_order α]
[mul_one_class α]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : 1 ≤ a) :
linear_order.min a b ≤ a * b
theorem
max_le_mul_of_one_le
{α : Type u_1}
[linear_order α]
[mul_one_class α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
{a b : α}
(ha : 1 ≤ a)
(hb : 1 ≤ b) :
linear_order.max a b ≤ a * b
theorem
max_le_add_of_nonneg
{α : Type u_1}
[linear_order α]
[add_zero_class α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
{a b : α}
(ha : 0 ≤ a)
(hb : 0 ≤ b) :
linear_order.max a b ≤ a + b