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_add_fn_max
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder α]
[inst : AddCommSemigroup β]
(f : α → β)
(n : α)
(m : α)
:
theorem
fn_min_mul_fn_max
{α : Type u_1}
{β : Type u_2}
[inst : LinearOrder α]
[inst : CommSemigroup β]
(f : α → β)
(n : α)
(m : α)
:
theorem
min_add_max
{α : Type u_1}
[inst : LinearOrder α]
[inst : AddCommSemigroup α]
(n : α)
(m : α)
:
theorem
min_mul_max
{α : Type u_1}
[inst : LinearOrder α]
[inst : CommSemigroup α]
(n : α)
(m : α)
:
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 : α)
:
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 : α)
:
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 : α)
:
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 : α)
:
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)
:
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)
:
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)
:
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)
:
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 : α)
:
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 : α)
:
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 : α)
:
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 : α)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
: