Mathlib.Algebra.Order.Monoid.Unbundled.MinMax

fn_min_mul_fn_max theorem

(f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b

Full source

@[to_additive]
lemma fn_min_mul_fn_max (f : α → β) (a b : α) : f (min a b) * f (max a b) = f a * f b := by
  obtain h | h := le_total a b <;> simp [h, mul_comm]

Product of Function Values at Minimum and Maximum Equals Product at Original Points

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ a commutative semigroup. For any function $f : \alpha \to \beta$ and elements $a, b \in \alpha$, we have $f(\min(a, b)) \cdot f(\max(a, b)) = f(a) \cdot f(b)$.

fn_max_mul_fn_min theorem

(f : α → β) (a b : α) : f (max a b) * f (min a b) = f a * f b

Full source

@[to_additive]
lemma fn_max_mul_fn_min (f : α → β) (a b : α) : f (max a b) * f (min a b) = f a * f b := by
  obtain h | h := le_total a b <;> simp [h, mul_comm]

Product of Function Values at Max and Min Equals Product at Original Points

Informal description

Let $\alpha$ be a linearly ordered type and $\beta$ be a commutative semigroup. For any function $f : \alpha \to \beta$ and any elements $a, b \in \alpha$, we have $f(\max(a, b)) \cdot f(\min(a, b)) = f(a) \cdot f(b)$.

min_mul_max theorem

(a b : α) : min a b * max a b = a * b

Full source

@[to_additive (attr := simp)]
lemma min_mul_max (a b : α) : min a b * max a b = a * b := fn_min_mul_fn_max id _ _

Product of Minimum and Maximum Equals Original Product in Ordered Semigroups

Informal description

Let $\alpha$ be a linearly ordered commutative semigroup. For any elements $a, b \in \alpha$, the product of the minimum and maximum of $a$ and $b$ equals the product of $a$ and $b$, i.e., $$\min(a, b) \cdot \max(a, b) = a \cdot b.$$

max_mul_min theorem

(a b : α) : max a b * min a b = a * b

Full source

@[to_additive (attr := simp)]
lemma max_mul_min (a b : α) : max a b * min a b = a * b := fn_max_mul_fn_min id _ _

Product of Max and Min Equals Original Product

Informal description

Let $\alpha$ be a linearly ordered type with a commutative multiplication operation. For any elements $a, b \in \alpha$, the product of the maximum and minimum of $a$ and $b$ equals the product of $a$ and $b$, i.e., $\max(a, b) \cdot \min(a, b) = a \cdot b$.

min_mul_mul_left theorem

(a b c : α) : min (a * b) (a * c) = a * min b c

Full source

@[to_additive]
theorem min_mul_mul_left (a b c : α) : min (a * b) (a * c) = a * min b c :=
  (monotone_id.const_mul' a).map_min.symm

$\min(a \cdot b, a \cdot c) = a \cdot \min(b, c)$ in a linearly ordered multiplicative structure

Informal description

For any elements $a, b, c$ in a linearly ordered multiplicative structure $\alpha$, the minimum of the products $a \cdot b$ and $a \cdot c$ is equal to the product of $a$ with the minimum of $b$ and $c$, i.e., $\min(a \cdot b, a \cdot c) = a \cdot \min(b, c)$.

max_mul_mul_left theorem

(a b c : α) : max (a * b) (a * c) = a * max b c

Full source

@[to_additive]
theorem max_mul_mul_left (a b c : α) : max (a * b) (a * c) = a * max b c :=
  (monotone_id.const_mul' a).map_max.symm

$\max(a \cdot b, a \cdot c) = a \cdot \max(b, c)$ in a linearly ordered multiplicative structure

Informal description

For any elements $a, b, c$ in a type $\alpha$ with a multiplication operation and a linear order, the maximum of the products $a \cdot b$ and $a \cdot c$ is equal to the product of $a$ with the maximum of $b$ and $c$, i.e., $\max(a \cdot b, a \cdot c) = a \cdot \max(b, c)$.

min_mul_mul_right theorem

(a b c : α) : min (a * c) (b * c) = min a b * c

Full source

@[to_additive]
theorem min_mul_mul_right (a b c : α) : min (a * c) (b * c) = min a b * c :=
  (monotone_id.mul_const' c).map_min.symm

$\min(a \cdot c, b \cdot c) = \min(a, b) \cdot c$ in a linearly ordered multiplicative structure

Informal description

For any elements $a, b, c$ in a type $\alpha$ with a multiplication operation and a linear order, the minimum of the products $a \cdot c$ and $b \cdot c$ is equal to the product of the minimum of $a$ and $b$ with $c$, i.e., $\min(a \cdot c, b \cdot c) = \min(a, b) \cdot c$.

max_mul_mul_right theorem

(a b c : α) : max (a * c) (b * c) = max a b * c

Full source

@[to_additive]
theorem max_mul_mul_right (a b c : α) : max (a * c) (b * c) = max a b * c :=
  (monotone_id.mul_const' c).map_max.symm

$\max(a \cdot c, b \cdot c) = \max(a, b) \cdot c$ in a linearly ordered multiplicative structure

Informal description

For any elements $a, b, c$ in a type $\alpha$ with a multiplication operation and a linear order, the maximum of the products $a \cdot c$ and $b \cdot c$ is equal to the product of the maximum of $a$ and $b$ with $c$, i.e., $\max(a \cdot c, b \cdot c) = \max(a, b) \cdot c$.

lt_or_lt_of_mul_lt_mul theorem

 [MulLeftMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} : a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂

Full source

@[to_additive]
theorem lt_or_lt_of_mul_lt_mul [MulLeftMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂ := by
  contrapose!
  exact fun h => mul_le_mul' h.1 h.2

Strict Inequality in Product Implies Strict Inequality in Factors

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-monotone and right-monotone. For any elements $a_1, a_2, b_1, b_2 \in \alpha$, if $a_1 * b_1 < a_2 * b_2$, then either $a_1 < a_2$ or $b_1 < b_2$.

le_or_lt_of_mul_le_mul theorem

 [MulLeftMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} : a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂

Full source

@[to_additive]
theorem le_or_lt_of_mul_le_mul [MulLeftMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂ := by
  contrapose!
  exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2

Disjunction of Inequalities from Multiplicative Inequality: $a_1b_1 \leq a_2b_2 \implies (a_1 \leq a_2) \lor (b_1 < b_2)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$) and right-strictly-monotone (i.e., $b < c$ implies $b \cdot a < c \cdot a$ for any $a$). Then for any elements $a_1, a_2, b_1, b_2 \in \alpha$, if $a_1 \cdot b_1 \leq a_2 \cdot b_2$, then either $a_1 \leq a_2$ or $b_1 < b_2$.

lt_or_le_of_mul_le_mul theorem

 [MulLeftStrictMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} : a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂

Full source

@[to_additive]
theorem lt_or_le_of_mul_le_mul [MulLeftStrictMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂ := by
  contrapose!
  exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2

Disjunction from Multiplication Inequality under Left-Strict and Right-Monotone Conditions: $a_1 \cdot b_1 \leq a_2 \cdot b_2 \implies (a_1 < a_2) \lor (b_1 \leq b_2)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-strictly-monotone (i.e., $b < c$ implies $a \cdot b < a \cdot c$ for any $a$) and right-monotone (i.e., $b \leq c$ implies $b \cdot a \leq c \cdot a$ for any $a$). Then for any elements $a_1, a_2, b_1, b_2 \in \alpha$ with $a_1 \cdot b_1 \leq a_2 \cdot b_2$, we have either $a_1 < a_2$ or $b_1 \leq b_2$.

le_or_le_of_mul_le_mul theorem

 [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} : a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂

Full source

@[to_additive]
theorem le_or_le_of_mul_le_mul [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂ := by
  contrapose!
  exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2

Disjunction of Inequalities from Multiplicative Inequality under Strict Monotonicity

Informal description

Let $\alpha$ be a type with a multiplication operation and a strict order such that multiplication is both left-strictly-monotone and right-strictly-monotone. Then for any elements $a_1, a_2, b_1, b_2 \in \alpha$, if $a_1 \cdot b_1 \leq a_2 \cdot b_2$, then either $a_1 \leq a_2$ or $b_1 \leq b_2$.

mul_lt_mul_iff_of_le_of_le theorem

 [MulLeftMono α] [MulRightMono α] [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂)
  (hb : b₁ ≤ b₂) : a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂

Full source

@[to_additive]
theorem mul_lt_mul_iff_of_le_of_le [MulLeftMono α]
    [MulRightMono α] [MulLeftStrictMono α]
    [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂)
    (hb : b₁ ≤ b₂) : a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂ := by
  refine ⟨lt_or_lt_of_mul_lt_mul, fun h => ?_⟩
  rcases h with ha' | hb'
  · exact mul_lt_mul_of_lt_of_le ha' hb
  · exact mul_lt_mul_of_le_of_lt ha hb'

Strict Inequality in Product Under Bounded Factors: $a_1 \leq a_2 \land b_1 \leq b_2 \implies (a_1 b_1 < a_2 b_2 \leftrightarrow a_1 < a_2 \lor b_1 < b_2)$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-monotone and right-monotone, and also both left-strictly-monotone and right-strictly-monotone. For any elements $a_1, a_2, b_1, b_2 \in \alpha$ with $a_1 \leq a_2$ and $b_1 \leq b_2$, we have the equivalence: $$a_1 \cdot b_1 < a_2 \cdot b_2 \iff (a_1 < a_2) \lor (b_1 < b_2).$$

min_le_mul_of_one_le_right theorem

[MulLeftMono α] {a b : α} (hb : 1 ≤ b) : min a b ≤ a * b

Full source

@[to_additive]
theorem min_le_mul_of_one_le_right [MulLeftMono α] {a b : α} (hb : 1 ≤ b) :
    min a b ≤ a * b :=
  min_le_iff.2 <| Or.inl <| le_mul_of_one_le_right' hb

Minimum Bound by Right Multiplication: $\min(a, b) \leq a \cdot b$ when $1 \leq b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is left-monotone (i.e., $b \leq c$ implies $a \cdot b \leq a \cdot c$ for any $a$). Then for any elements $a, b \in \alpha$ with $1 \leq b$, the minimum of $a$ and $b$ is less than or equal to $a \cdot b$, i.e., $\min(a, b) \leq a \cdot b$.

min_le_mul_of_one_le_left theorem

[MulRightMono α] {a b : α} (ha : 1 ≤ a) : min a b ≤ a * b

Full source

@[to_additive]
theorem min_le_mul_of_one_le_left [MulRightMono α] {a b : α} (ha : 1 ≤ a) :
    min a b ≤ a * b :=
  min_le_iff.2 <| Or.inr <| le_mul_of_one_le_left' ha

Minimum Bound by Product under Right Monotonicity: $\min(a, b) \leq a * b$ when $1 \leq a$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is right-monotone (i.e., $b \leq c$ implies $a * b \leq a * c$ for any $a$). For any elements $a, b \in \alpha$ with $1 \leq a$, the minimum of $a$ and $b$ is less than or equal to their product, i.e., $\min(a, b) \leq a * b$.

max_le_mul_of_one_le theorem

[MulLeftMono α] [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) : max a b ≤ a * b

Full source

@[to_additive]
theorem max_le_mul_of_one_le [MulLeftMono α] [MulRightMono α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
    max a b ≤ a * b :=
  max_le_iff.2 ⟨le_mul_of_one_le_right' hb, le_mul_of_one_le_left' ha⟩

Maximum Bound by Product under Monotonicity: $\max(a, b) \leq a * b$ when $1 \leq a, b$

Informal description

Let $\alpha$ be a type with a multiplication operation and a partial order such that multiplication is both left-monotone and right-monotone. For any elements $a, b \in \alpha$ satisfying $1 \leq a$ and $1 \leq b$, the maximum of $a$ and $b$ is less than or equal to their product, i.e., $\max(a, b) \leq a * b$.