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} [LinearOrder α] [AddCommSemigroup β] (f : α → β) (a : α) (b : α) : f (min a b) + f (max a b) = f a + f b

theorem fn_min_mul_fn_max {α : Type u_1} {β : Type u_2} [LinearOrder α] [CommSemigroup β] (f : α → β) (a : α) (b : α) : f (min a b) * f (max a b) = f a * f b

theorem fn_max_add_fn_min {α : Type u_1} {β : Type u_2} [LinearOrder α] [AddCommSemigroup β] (f : α → β) (a : α) (b : α) : f (max a b) + f (min a b) = f a + f b

theorem fn_max_mul_fn_min {α : Type u_1} {β : Type u_2} [LinearOrder α] [CommSemigroup β] (f : α → β) (a : α) (b : α) : f (max a b) * f (min a b) = f a * f b

@[simp]

theorem min_add_max {α : Type u_1} [LinearOrder α] [AddCommSemigroup α] (a : α) (b : α) : min a b + max a b = a + b

@[simp]

theorem min_mul_max {α : Type u_1} [LinearOrder α] [CommSemigroup α] (a : α) (b : α) : min a b * max a b = a * b

@[simp]

theorem max_add_min {α : Type u_1} [LinearOrder α] [AddCommSemigroup α] (a : α) (b : α) : max a b + min a b = a + b

@[simp]

theorem max_mul_min {α : Type u_1} [LinearOrder α] [CommSemigroup α] (a : α) (b : α) : max a b * min a b = a * b

theorem min_add_add_left {α : Type u_1} [LinearOrder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : min (a + b) (a + c) = a + min b c

theorem min_mul_mul_left {α : Type u_1} [LinearOrder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : min (a * b) (a * c) = a * min b c

theorem max_add_add_left {α : Type u_1} [LinearOrder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : max (a + b) (a + c) = a + max b c

theorem max_mul_mul_left {α : Type u_1} [LinearOrder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : max (a * b) (a * c) = a * max b c

theorem min_add_add_right {α : Type u_1} [LinearOrder α] [Add α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : min (a + c) (b + c) = min a b + c

theorem min_mul_mul_right {α : Type u_1} [LinearOrder α] [Mul α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : min (a * c) (b * c) = min a b * c

theorem max_add_add_right {α : Type u_1} [LinearOrder α] [Add α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : max (a + c) (b + c) = max a b + c

theorem max_mul_mul_right {α : Type u_1} [LinearOrder α] [Mul α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] (a : α) (b : α) (c : α) : max (a * c) (b * c) = max a b * c

theorem lt_or_lt_of_add_lt_add {α : Type u_1} [LinearOrder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} : a₁ + b₁ < a₂ + b₂ → a₁ < a₂ ∨ b₁ < b₂

theorem lt_or_lt_of_mul_lt_mul {α : Type u_1} [LinearOrder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {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 α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {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 α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {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 α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {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 α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {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 α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {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 α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} : a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂

theorem add_lt_add_iff_of_le_of_le {α : Type u_1} [LinearOrder α] [Add α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₁ + b₁ < a₂ + b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

theorem mul_lt_mul_iff_of_le_of_le {α : Type u_1} [LinearOrder α] [Mul α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {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} [LinearOrder α] [AddZeroClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (hb : 0 ≤ b) : min a b ≤ a + b

theorem min_le_mul_of_one_le_right {α : Type u_1} [LinearOrder α] [MulOneClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (hb : 1 ≤ b) : min a b ≤ a * b

theorem min_le_add_of_nonneg_left {α : Type u_1} [LinearOrder α] [AddZeroClass α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (ha : 0 ≤ a) : min a b ≤ a + b

theorem min_le_mul_of_one_le_left {α : Type u_1} [LinearOrder α] [MulOneClass α] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (ha : 1 ≤ a) : min a b ≤ a * b

theorem max_le_add_of_nonneg {α : Type u_1} [LinearOrder α] [AddZeroClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : max a b ≤ a + b

theorem max_le_mul_of_one_le {α : Type u_1} [LinearOrder α] [MulOneClass α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] [CovariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {a : α} {b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : max a b ≤ a * b