min and max in linearly ordered groups.

@[simp]

theorem max_one_div_max_inv_one_eq_self {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : (a ⊔ 1) / (a⁻¹ ⊔ 1) = a

@[simp]

theorem max_zero_sub_max_neg_zero_eq_self {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] (a : α) : a ⊔ 0 - -a ⊔ 0 = a

theorem max_zero_sub_eq_self {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] (a : α) : a ⊔ 0 - -a ⊔ 0 = a

Alias of max_zero_sub_max_neg_zero_eq_self.

theorem max_inv_one {α : Type u_1} [Group α] [LinearOrder α] [MulLeftMono α] (a : α) : a⁻¹ ⊔ 1 = a⁻¹ * (a ⊔ 1)

theorem max_neg_zero {α : Type u_1} [AddGroup α] [LinearOrder α] [AddLeftMono α] (a : α) : -a ⊔ 0 = -a + a ⊔ 0

theorem min_inv_inv' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) : a⁻¹ ⊓ b⁻¹ = (a ⊔ b)⁻¹

theorem min_neg_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : -a ⊓ -b = -(a ⊔ b)

theorem max_inv_inv' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) : a⁻¹ ⊔ b⁻¹ = (a ⊓ b)⁻¹

theorem max_neg_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : -a ⊔ -b = -(a ⊓ b)

theorem min_div_div_right' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : a / c ⊓ b / c = (a ⊓ b) / c

theorem min_sub_sub_right {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : (a - c) ⊓ (b - c) = a ⊓ b - c

theorem max_div_div_right' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : a / c ⊔ b / c = (a ⊔ b) / c

theorem max_sub_sub_right {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : (a - c) ⊔ (b - c) = a ⊔ b - c

theorem min_div_div_left' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : a / b ⊓ a / c = a / (b ⊔ c)

theorem min_sub_sub_left {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : (a - b) ⊓ (a - c) = a - b ⊔ c

theorem max_div_div_left' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : a / b ⊔ a / c = a / (b ⊓ c)

theorem max_sub_sub_left {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : (a - b) ⊔ (a - c) = a - b ⊓ c

theorem max_sub_max_le_max {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) : a ⊔ b - c ⊔ d ≤ (a - c) ⊔ (b - d)

theorem abs_max_sub_max_le_max {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) : |a ⊔ b - c ⊔ d| ≤ |a - c| ⊔ |b - d|

theorem abs_min_sub_min_le_max {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) : |a ⊓ b - c ⊓ d| ≤ |a - c| ⊔ |b - d|

theorem abs_max_sub_max_le_abs {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : |a ⊔ c - b ⊔ c| ≤ |a - b|