mathlib documentation

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 α] [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 : α) :
theorem min_mul_max {α : Type u_1} [linear_order α] [comm_semigroup α] (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 : α) :
theorem min_add_add_left {α : Type u_1} [linear_order α] [has_add α] [covariant_class α α has_add.add has_le.le] (a 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 : α) :
theorem max_mul_mul_left {α : Type u_1} [linear_order α] [has_mul α] [covariant_class α α has_mul.mul has_le.le] (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 b m n : α} (h : m + n < a + b) :
m < a n < 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 b m n : α} (h : m * n < a * b) :
m < a n < b
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 : α) :
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 : α) :
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 : α) :
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 : α) :
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) :
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) :