Mathlib.Order.MinMax

le_min_iff theorem

: c ≤ min a b ↔ c ≤ a ∧ c ≤ b

Full source

theorem le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b :=
  le_inf_iff

Characterization of Minimum Bound: $c \leq \min(a, b) \leftrightarrow (c \leq a \land c \leq b)$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the inequality $c \leq \min(a, b)$ holds if and only if both $c \leq a$ and $c \leq b$ hold.

le_max_iff theorem

: a ≤ max b c ↔ a ≤ b ∨ a ≤ c

Full source

theorem le_max_iff : a ≤ max b c ↔ a ≤ b ∨ a ≤ c :=
  le_sup_iff

Order Characterization of Maximum: $a \leq \max(b, c) \leftrightarrow (a \leq b \lor a \leq c)$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, $a$ is less than or equal to the maximum of $b$ and $c$ if and only if $a \leq b$ or $a \leq c$. In symbols: \[ a \leq \max(b, c) \leftrightarrow (a \leq b \lor a \leq c). \]

min_le_iff theorem

: min a b ≤ c ↔ a ≤ c ∨ b ≤ c

Full source

theorem min_le_iff : minmin a b ≤ c ↔ a ≤ c ∨ b ≤ c :=
  inf_le_iff

Minimum Bound Characterization: $\min(a, b) \leq c \leftrightarrow (a \leq c \lor b \leq c)$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the minimum of $a$ and $b$ is less than or equal to $c$ if and only if $a \leq c$ or $b \leq c$. In symbols: \[ \min(a, b) \leq c \leftrightarrow (a \leq c \lor b \leq c). \]

max_le_iff theorem

: max a b ≤ c ↔ a ≤ c ∧ b ≤ c

Full source

theorem max_le_iff : maxmax a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
  sup_le_iff

Maximum Bound Criterion: $\max(a, b) \leq c \leftrightarrow (a \leq c \land b \leq c)$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the maximum of $a$ and $b$ is less than or equal to $c$ if and only if both $a \leq c$ and $b \leq c$. In symbols: \[ \max(a, b) \leq c \leftrightarrow (a \leq c \land b \leq c). \]

lt_min_iff theorem

: a < min b c ↔ a < b ∧ a < c

Full source

theorem lt_min_iff : a < min b c ↔ a < b ∧ a < c :=
  lt_inf_iff

Characterization of Strict Inequality Under Minimum: $a < \min(b, c) \leftrightarrow a < b \land a < c$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the inequality $a < \min(b, c)$ holds if and only if both $a < b$ and $a < c$ hold. In symbols: \[ a < \min(b, c) \leftrightarrow a < b \land a < c. \]

lt_max_iff theorem

: a < max b c ↔ a < b ∨ a < c

Full source

theorem lt_max_iff : a < max b c ↔ a < b ∨ a < c :=
  lt_sup_iff

Characterization of Strict Inequality Under Maximum: $a < \max(b, c) \leftrightarrow a < b \lor a < c$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the inequality $a < \max(b, c)$ holds if and only if either $a < b$ or $a < c$ holds. In symbols: \[ a < \max(b, c) \leftrightarrow a < b \lor a < c. \]

min_lt_iff theorem

: min a b < c ↔ a < c ∨ b < c

Full source

theorem min_lt_iff : minmin a b < c ↔ a < c ∨ b < c :=
  inf_lt_iff

Characterization of $\min(a, b) < c$ in Linear Orders

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the minimum of $a$ and $b$ is strictly less than $c$ if and only if either $a < c$ or $b < c$ holds. In symbols: \[ \min(a, b) < c \leftrightarrow a < c \lor b < c. \]

max_lt_iff theorem

: max a b < c ↔ a < c ∧ b < c

Full source

theorem max_lt_iff : maxmax a b < c ↔ a < c ∧ b < c :=
  sup_lt_iff

Characterization of $\max(a, b) < c$ in Linear Orders

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the maximum of $a$ and $b$ is strictly less than $c$ if and only if both $a$ and $b$ are strictly less than $c$. In symbols: \[ \max(a, b) < c \leftrightarrow a < c \land b < c. \]

max_le_max theorem

: a ≤ c → b ≤ d → max a b ≤ max c d

Full source

theorem max_le_max : a ≤ c → b ≤ d → max a b ≤ max c d :=
  sup_le_sup

Monotonicity of Maximum: $a \leq c \land b \leq d \Rightarrow \max(a, b) \leq \max(c, d)$

Informal description

For any elements $a, b, c, d$ in a linearly ordered set, if $a \leq c$ and $b \leq d$, then $\max(a, b) \leq \max(c, d)$.

max_le_max_left theorem

(c) (h : a ≤ b) : max c a ≤ max c b

Full source

theorem max_le_max_left (c) (h : a ≤ b) : max c a ≤ max c b := sup_le_sup_left h c

Left Monotonicity of Maximum: $\max(c, a) \leq \max(c, b)$ when $a \leq b$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a \leq b$, then $\max(c, a) \leq \max(c, b)$.

max_le_max_right theorem

(c) (h : a ≤ b) : max a c ≤ max b c

Full source

theorem max_le_max_right (c) (h : a ≤ b) : max a c ≤ max b c := sup_le_sup_right h c

Right Monotonicity of Maximum: $a \leq b \Rightarrow \max(a, c) \leq \max(b, c)$

Informal description

For any elements $a, b, c$ in a linearly ordered set, if $a \leq b$, then $\max(a, c) \leq \max(b, c)$.

min_le_min theorem

: a ≤ c → b ≤ d → min a b ≤ min c d

Full source

theorem min_le_min : a ≤ c → b ≤ d → min a b ≤ min c d :=
  inf_le_inf

Monotonicity of Minimum Operation: $a \leq c \land b \leq d \Rightarrow \min(a, b) \leq \min(c, d)$

Informal description

For any elements $a, b, c, d$ in a linearly ordered set, if $a \leq c$ and $b \leq d$, then the minimum of $a$ and $b$ is less than or equal to the minimum of $c$ and $d$, i.e., $\min(a, b) \leq \min(c, d)$.

min_le_min_left theorem

(c) (h : a ≤ b) : min c a ≤ min c b

Full source

theorem min_le_min_left (c) (h : a ≤ b) : min c a ≤ min c b := inf_le_inf_left c h

Left Monotonicity of Minimum Operation: $a \leq b \Rightarrow \min(c, a) \leq \min(c, b)$

Informal description

For any elements $a, b, c$ in a linearly ordered set, if $a \leq b$, then $\min(c, a) \leq \min(c, b)$.

min_le_min_right theorem

(c) (h : a ≤ b) : min a c ≤ min b c

Full source

theorem min_le_min_right (c) (h : a ≤ b) : min a c ≤ min b c := inf_le_inf_right c h

Right Monotonicity of Minimum Operation: $a \leq b \Rightarrow \min(a, c) \leq \min(b, c)$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a \leq b$, then $\min(a, c) \leq \min(b, c)$.

le_max_of_le_left theorem

: a ≤ b → a ≤ max b c

Full source

theorem le_max_of_le_left : a ≤ b → a ≤ max b c :=
  le_sup_of_le_left

Left Inequality Implies Maximum Inequality

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a \leq b$, then $a \leq \max(b, c)$.

le_max_of_le_right theorem

: a ≤ c → a ≤ max b c

Full source

theorem le_max_of_le_right : a ≤ c → a ≤ max b c :=
  le_sup_of_le_right

Right Inequality Implies Maximum Inequality

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a \leq c$, then $a \leq \max(b, c)$.

lt_max_of_lt_left theorem

(h : a < b) : a < max b c

Full source

theorem lt_max_of_lt_left (h : a < b) : a < max b c :=
  h.trans_le (le_max_left b c)

Strict Inequality Preserved Under Maximum on Left

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a < b$, then $a < \max(b, c)$.

lt_max_of_lt_right theorem

(h : a < c) : a < max b c

Full source

theorem lt_max_of_lt_right (h : a < c) : a < max b c :=
  h.trans_le (le_max_right b c)

Strict Inequality Preserved Under Maximum on the Right

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a < c$, then $a < \max(b, c)$.

min_le_of_left_le theorem

: a ≤ c → min a b ≤ c

Full source

theorem min_le_of_left_le : a ≤ c → min a b ≤ c :=
  inf_le_of_left_le

Minimum is Less Than or Equal to Right Argument When Left Argument Is

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a \leq c$, then the minimum of $a$ and $b$ is less than or equal to $c$, i.e., $\min(a, b) \leq c$.

min_le_of_right_le theorem

: b ≤ c → min a b ≤ c

Full source

theorem min_le_of_right_le : b ≤ c → min a b ≤ c :=
  inf_le_of_right_le

Minimum is Less Than or Equal to Right Argument When Right Argument Is

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $b \leq c$, then the minimum of $a$ and $b$ is less than or equal to $c$.

min_lt_of_left_lt theorem

(h : a < c) : min a b < c

Full source

theorem min_lt_of_left_lt (h : a < c) : min a b < c :=
  (min_le_left a b).trans_lt h

Minimum is Less Than if Left Argument is Less Than

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, if $a < c$, then $\min(a, b) < c$.

min_lt_of_right_lt theorem

(h : b < c) : min a b < c

Full source

theorem min_lt_of_right_lt (h : b < c) : min a b < c :=
  (min_le_right a b).trans_lt h

Minimum with Right Element Less Than Another Element is Less Than That Element

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, if $b < c$, then $\min(a, b) < c$.

max_min_distrib_left theorem

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

Full source

lemma max_min_distrib_left (a b c : α) : max a (min b c) = min (max a b) (max a c) :=
  sup_inf_left _ _ _

Left Distributivity of Maximum over Minimum: $\max(a, \min(b, c)) = \min(\max(a, b), \max(a, c))$

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, the following equality holds: $$ \max(a, \min(b, c)) = \min(\max(a, b), \max(a, c)). $$

max_min_distrib_right theorem

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

Full source

lemma max_min_distrib_right (a b c : α) : max (min a b) c = min (max a c) (max b c) :=
  sup_inf_right _ _ _

Right Distributivity of Maximum over Minimum: $\max(\min(a, b), c) = \min(\max(a, c), \max(b, c))$

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, the following equality holds: $$\max(\min(a, b), c) = \min(\max(a, c), \max(b, c)).$$

min_max_distrib_left theorem

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

Full source

lemma min_max_distrib_left (a b c : α) : min a (max b c) = max (min a b) (min a c) :=
  inf_sup_left _ _ _

Left Distributivity of Minimum over Maximum: $\min(a, \max(b, c)) = \max(\min(a, b), \min(a, c))$

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, the following equality holds: $$ \min(a, \max(b, c)) = \max(\min(a, b), \min(a, c)). $$

min_max_distrib_right theorem

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

Full source

lemma min_max_distrib_right (a b c : α) : min (max a b) c = max (min a c) (min b c) :=
  inf_sup_right _ _ _

Right Distributivity of Minimum over Maximum: $\min(\max(a, b), c) = \max(\min(a, c), \min(b, c))$

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, the following equality holds: $$\min(\max(a, b), c) = \max(\min(a, c), \min(b, c)).$$

min_le_max theorem

: min a b ≤ max a b

Full source

theorem min_le_max : min a b ≤ max a b :=
  le_trans (min_le_left a b) (le_max_left a b)

$\min(a,b) \leq \max(a,b)$ in a linear order

Informal description

For any two elements $a$ and $b$ in a linearly ordered set, the minimum of $a$ and $b$ is less than or equal to the maximum of $a$ and $b$.

min_eq_left_iff theorem

: min a b = a ↔ a ≤ b

Full source

theorem min_eq_left_iff : minmin a b = a ↔ a ≤ b :=
  inf_eq_left

Minimum Equals Left Element if and only if Left is Less Than or Equal to Right

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the minimum of $a$ and $b$ equals $a$ if and only if $a \leq b$.

min_eq_right_iff theorem

: min a b = b ↔ b ≤ a

Full source

theorem min_eq_right_iff : minmin a b = b ↔ b ≤ a :=
  inf_eq_right

Minimum Equals Right Element if and only if Right is Less Than or Equal to Left

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the minimum of $a$ and $b$ equals $b$ if and only if $b \leq a$.

max_eq_left_iff theorem

: max a b = a ↔ b ≤ a

Full source

theorem max_eq_left_iff : maxmax a b = a ↔ b ≤ a :=
  sup_eq_left

Maximum Equals Left Element if and only if Right is Less Than or Equal to Left

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the maximum of $a$ and $b$ equals $a$ if and only if $b \leq a$.

max_eq_right_iff theorem

: max a b = b ↔ a ≤ b

Full source

theorem max_eq_right_iff : maxmax a b = b ↔ a ≤ b :=
  sup_eq_right

Characterization of Maximum: $\max(a, b) = b \leftrightarrow a \leq b$

Informal description

For any elements $a$ and $b$ in a linearly ordered set, the maximum $\max(a, b)$ equals $b$ if and only if $a \leq b$.

min_cases theorem

(a b : α) : min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a

Full source

/-- For elements `a` and `b` of a linear order, either `min a b = a` and `a ≤ b`,
    or `min a b = b` and `b < a`.
    Use cases on this lemma to automate linarith in inequalities -/
theorem min_cases (a b : α) : minmin a b = a ∧ a ≤ bmin a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a := by
  by_cases h : a ≤ b
  · left
    exact ⟨min_eq_left h, h⟩
  · right
    exact ⟨min_eq_right (le_of_lt (not_le.mp h)), not_le.mp h⟩

Characterization of Minimum: $\min(a, b) = a \land a \leq b$ or $\min(a, b) = b \land b < a$

Informal description

For any elements $a$ and $b$ in a linear order, either the minimum $\min(a, b)$ equals $a$ and $a \leq b$, or $\min(a, b)$ equals $b$ and $b < a$.

max_cases theorem

(a b : α) : max a b = a ∧ b ≤ a ∨ max a b = b ∧ a < b

Full source

/-- For elements `a` and `b` of a linear order, either `max a b = a` and `b ≤ a`,
    or `max a b = b` and `a < b`.
    Use cases on this lemma to automate linarith in inequalities -/
theorem max_cases (a b : α) : maxmax a b = a ∧ b ≤ amax a b = a ∧ b ≤ a ∨ max a b = b ∧ a < b :=
  @min_cases αᵒᵈ _ a b

Characterization of Maximum: $\max(a, b) = a \land b \leq a$ or $\max(a, b) = b \land a < b$

Informal description

For any elements $a$ and $b$ in a linear order, either the maximum $\max(a, b)$ equals $a$ and $b \leq a$, or $\max(a, b)$ equals $b$ and $a < b$.

min_eq_iff theorem

: min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a

Full source

theorem min_eq_iff : minmin a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a := by
  constructor
  · intro h
    refine Or.imp (fun h' => ?_) (fun h' => ?_) (le_total a b) <;> exact ⟨by simpa [h'] using h, h'⟩
  · rintro (⟨rfl, h⟩ | ⟨rfl, h⟩) <;> simp [h]

Characterization of Minimum Equality in Linear Orders

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set $\alpha$, the minimum of $a$ and $b$ equals $c$ if and only if either ($a = c$ and $a \leq b$) or ($b = c$ and $b \leq a$).

max_eq_iff theorem

: max a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b

Full source

theorem max_eq_iff : maxmax a b = c ↔ a = c ∧ b ≤ a ∨ b = c ∧ a ≤ b :=
  @min_eq_iff αᵒᵈ _ a b c

Characterization of Maximum Equality in Linear Orders

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the maximum of $a$ and $b$ equals $c$ if and only if either ($a = c$ and $b \leq a$) or ($b = c$ and $a \leq b$).

min_lt_min_left_iff theorem

: min a c < min b c ↔ a < b ∧ a < c

Full source

theorem min_lt_min_left_iff : minmin a c < min b c ↔ a < b ∧ a < c := by
  simp_rw [lt_min_iff, min_lt_iff, or_iff_left (lt_irrefl _)]
  exact and_congr_left fun h => or_iff_left_of_imp h.trans

Inequality of Minima: $\min(a, c) < \min(b, c) \leftrightarrow a < b \land a < c$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the minimum of $a$ and $c$ is less than the minimum of $b$ and $c$ if and only if $a$ is less than $b$ and $a$ is less than $c$. In symbols: \[ \min(a, c) < \min(b, c) \leftrightarrow a < b \land a < c. \]

min_lt_min_right_iff theorem

: min a b < min a c ↔ b < c ∧ b < a

Full source

theorem min_lt_min_right_iff : minmin a b < min a c ↔ b < c ∧ b < a := by
  simp_rw [min_comm a, min_lt_min_left_iff]

$\min(a, b) < \min(a, c) \leftrightarrow (b < c \land b < a)$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the inequality $\min(a, b) < \min(a, c)$ holds if and only if both $b < c$ and $b < a$ hold.

max_lt_max_left_iff theorem

: max a c < max b c ↔ a < b ∧ c < b

Full source

theorem max_lt_max_left_iff : maxmax a c < max b c ↔ a < b ∧ c < b :=
  @min_lt_min_left_iff αᵒᵈ _ _ _ _

Inequality of Maxima: $\max(a, c) < \max(b, c) \leftrightarrow a < b \land c < b$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the maximum of $a$ and $c$ is less than the maximum of $b$ and $c$ if and only if $a$ is less than $b$ and $c$ is less than $b$. In symbols: \[ \max(a, c) < \max(b, c) \leftrightarrow a < b \land c < b. \]

max_lt_max_right_iff theorem

: max a b < max a c ↔ b < c ∧ a < c

Full source

theorem max_lt_max_right_iff : maxmax a b < max a c ↔ b < c ∧ a < c :=
  @min_lt_min_right_iff αᵒᵈ _ _ _ _

$\max(a, b) < \max(a, c) \leftrightarrow (b < c \land a < c)$

Informal description

For any elements $a$, $b$, and $c$ in a linearly ordered set, the inequality $\max(a, b) < \max(a, c)$ holds if and only if both $b < c$ and $a < c$ hold.

max_idem instance

: Std.IdempotentOp (α := α) max

Full source

/-- An instance asserting that `max a a = a` -/
instance max_idem : Std.IdempotentOp (α := α) max where
  idempotent := by simp

Idempotence of the Maximum Operation in Linear Orders

Informal description

For any linearly ordered set $\alpha$ and element $a \in \alpha$, the maximum operation satisfies $\max(a, a) = a$.

min_idem instance

: Std.IdempotentOp (α := α) min

Full source

/-- An instance asserting that `min a a = a` -/
instance min_idem : Std.IdempotentOp (α := α) min where
  idempotent := by simp

Idempotence of the Minimum Operation in Linear Orders

Informal description

For any linearly ordered set $\alpha$, the minimum operation is idempotent, meaning $\min(a, a) = a$ for any element $a \in \alpha$.

min_lt_max theorem

: min a b < max a b ↔ a ≠ b

Full source

theorem min_lt_max : minmin a b < max a b ↔ a ≠ b :=
  inf_lt_sup

Minimum Strictly Less Than Maximum iff Elements Are Distinct ($\min(a, b) < \max(a, b) \leftrightarrow a \neq b$)

Informal description

For any two elements $a$ and $b$ in a linearly ordered set, the minimum of $a$ and $b$ is strictly less than their maximum if and only if $a$ and $b$ are distinct, i.e., $\min(a, b) < \max(a, b) \leftrightarrow a \neq b$.

max_lt_max theorem

(h₁ : a < c) (h₂ : b < d) : max a b < max c d

Full source

theorem max_lt_max (h₁ : a < c) (h₂ : b < d) : max a b < max c d :=
  max_lt (lt_max_of_lt_left h₁) (lt_max_of_lt_right h₂)

Maximum Preserves Strict Inequality: $\max(a, b) < \max(c, d)$ under $a < c$ and $b < d$

Informal description

For any elements $a, b, c, d$ in a linearly ordered set, if $a < c$ and $b < d$, then $\max(a, b) < \max(c, d)$.

min_lt_min theorem

(h₁ : a < c) (h₂ : b < d) : min a b < min c d

Full source

theorem min_lt_min (h₁ : a < c) (h₂ : b < d) : min a b < min c d :=
  @max_lt_max αᵒᵈ _ _ _ _ _ h₁ h₂

Minimum Preserves Strict Inequality: $\min(a, b) < \min(c, d)$ under $a < c$ and $b < d$

Informal description

For any elements $a, b, c, d$ in a linearly ordered set, if $a < c$ and $b < d$, then $\min(a, b) < \min(c, d)$.

min_right_comm theorem

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

Full source

theorem min_right_comm (a b c : α) : min (min a b) c = min (min a c) b := by
  rw [min_assoc, min_comm b, min_assoc]

Right Commutativity of Minimum Operation

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, the minimum operation satisfies the right-commutativity property: \[ \min(\min(a, b), c) = \min(\min(a, c), b). \]

Max.left_comm theorem

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

Full source

theorem Max.left_comm (a b c : α) : max a (max b c) = max b (max a c) := by
  rw [← max_assoc, max_comm a, max_assoc]

Left Commutativity of Maximum Operation

Informal description

For any three elements $a, b, c$ in a linearly ordered set $\alpha$, the maximum operation satisfies the left commutativity property: \[ \max(a, \max(b, c)) = \max(b, \max(a, c)) \]

Max.right_comm theorem

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

Full source

theorem Max.right_comm (a b c : α) : max (max a b) c = max (max a c) b := by
  rw [max_assoc, max_comm b, max_assoc]

Right Commutativity of Maximum Operation in Linear Orders

Informal description

For any three elements $a, b, c$ in a linearly ordered set $\alpha$, the maximum operation satisfies the right commutativity property: \[ \max(\max(a, b), c) = \max(\max(a, c), b) \]

MonotoneOn.map_max theorem

(hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (max a b) = max (f a) (f b)

Full source

theorem MonotoneOn.map_max (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (max a b) =
    max (f a) (f b) := by
  rcases le_total a b with h | h <;>
    simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

Monotonicity Preserves Maximum: $f(\max(a, b)) = \max(f(a), f(b))$

Informal description

Let $f$ be a function defined on a set $s$ in a linearly ordered set $\alpha$, and suppose $f$ is monotone on $s$. For any two elements $a, b \in s$, the image of the maximum of $a$ and $b$ under $f$ is equal to the maximum of the images of $a$ and $b$ under $f$, i.e., $f(\max(a, b)) = \max(f(a), f(b))$.

MonotoneOn.map_min theorem

(hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (min a b) = min (f a) (f b)

Full source

theorem MonotoneOn.map_min (hf : MonotoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (min a b) =
    min (f a) (f b) := hf.dual.map_max ha hb

Monotonicity Preserves Minimum: $f(\min(a, b)) = \min(f(a), f(b))$

Informal description

Let $f$ be a function defined on a subset $s$ of a linearly ordered set $\alpha$, and suppose $f$ is monotone on $s$. For any two elements $a, b \in s$, the image of the minimum of $a$ and $b$ under $f$ is equal to the minimum of the images of $a$ and $b$ under $f$, i.e., $f(\min(a, b)) = \min(f(a), f(b))$.

AntitoneOn.map_max theorem

(hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (max a b) = min (f a) (f b)

Full source

theorem AntitoneOn.map_max (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (max a b) =
    min (f a) (f b) := hf.dual_right.map_max ha hb

Antitone Function Maps Maximum to Minimum: $f(\max(a, b)) = \min(f(a), f(b))$

Informal description

Let $f$ be a function defined on a subset $s$ of a linearly ordered set, and suppose $f$ is antitone on $s$. For any two elements $a, b \in s$, the image of the maximum of $a$ and $b$ under $f$ is equal to the minimum of the images of $a$ and $b$ under $f$, i.e., $f(\max(a, b)) = \min(f(a), f(b))$.

AntitoneOn.map_min theorem

(hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (min a b) = max (f a) (f b)

Full source

theorem AntitoneOn.map_min (hf : AntitoneOn f s) (ha : a ∈ s) (hb : b ∈ s) : f (min a b) =
    max (f a) (f b) := hf.dual.map_max ha hb

Antitone Function Maps Minimum to Maximum: $f(\min(a, b)) = \max(f(a), f(b))$

Informal description

Let $f$ be a function defined on a subset $s$ of a linearly ordered set, and suppose $f$ is antitone on $s$. For any two elements $a, b \in s$, the image of the minimum of $a$ and $b$ under $f$ is equal to the maximum of the images of $a$ and $b$ under $f$, i.e., $f(\min(a, b)) = \max(f(a), f(b))$.

Monotone.map_max theorem

(hf : Monotone f) : f (max a b) = max (f a) (f b)

Full source

theorem Monotone.map_max (hf : Monotone f) : f (max a b) = max (f a) (f b) := by
  rcases le_total a b with h | h <;> simp [h, hf h]

Monotonicity Preserves Maximum: $f(\max(a, b)) = \max(f(a), f(b))$

Informal description

For any monotone function $f$ and elements $a, b$ in its domain, the image of the maximum of $a$ and $b$ under $f$ is equal to the maximum of the images $f(a)$ and $f(b)$, i.e., $f(\max(a, b)) = \max(f(a), f(b))$.

Monotone.map_min theorem

(hf : Monotone f) : f (min a b) = min (f a) (f b)

Full source

theorem Monotone.map_min (hf : Monotone f) : f (min a b) = min (f a) (f b) :=
  hf.dual.map_max

Monotonicity Preserves Minimum: $f(\min(a, b)) = \min(f(a), f(b))$

Informal description

For any monotone function $f$ and elements $a, b$ in its domain, the image of the minimum of $a$ and $b$ under $f$ is equal to the minimum of the images $f(a)$ and $f(b)$, i.e., $f(\min(a, b)) = \min(f(a), f(b))$.

Antitone.map_max theorem

(hf : Antitone f) : f (max a b) = min (f a) (f b)

Full source

theorem Antitone.map_max (hf : Antitone f) : f (max a b) = min (f a) (f b) := by
  rcases le_total a b with h | h <;> simp [h, hf h]

Antitone Function Maps Maximum to Minimum: $f(\max(a, b)) = \min(f(a), f(b))$

Informal description

For any antitone function $f$ and elements $a, b$ in its domain, the image of the maximum of $a$ and $b$ under $f$ is equal to the minimum of the images $f(a)$ and $f(b)$, i.e., $f(\max(a, b)) = \min(f(a), f(b))$.

Antitone.map_min theorem

(hf : Antitone f) : f (min a b) = max (f a) (f b)

Full source

theorem Antitone.map_min (hf : Antitone f) : f (min a b) = max (f a) (f b) :=
  hf.dual.map_max

Antitone Function Maps Minimum to Maximum: $f(\min(a, b)) = \max(f(a), f(b))$

Informal description

For any antitone function $f$ and elements $a, b$ in its domain, the image of the minimum of $a$ and $b$ under $f$ is equal to the maximum of the images $f(a)$ and $f(b)$, i.e., $f(\min(a, b)) = \max(f(a), f(b))$.

min_choice theorem

(a b : α) : min a b = a ∨ min a b = b

Full source

theorem min_choice (a b : α) : minmin a b = a ∨ min a b = b := by cases le_total a b <;> simp [*]

Minimum Choice Property: $\min(a, b) = a \lor \min(a, b) = b$

Informal description

For any two elements $a$ and $b$ in a linearly ordered set $\alpha$, the minimum of $a$ and $b$ is either equal to $a$ or equal to $b$.

max_choice theorem

(a b : α) : max a b = a ∨ max a b = b

Full source

theorem max_choice (a b : α) : maxmax a b = a ∨ max a b = b :=
  @min_choice αᵒᵈ _ a b

Maximum Choice Property: $\max(a, b) = a \lor \max(a, b) = b$

Informal description

For any two elements $a$ and $b$ in a linearly ordered set $\alpha$, the maximum of $a$ and $b$ is either equal to $a$ or equal to $b$.

le_of_max_le_left theorem

{a b c : α} (h : max a b ≤ c) : a ≤ c

Full source

theorem le_of_max_le_left {a b c : α} (h : max a b ≤ c) : a ≤ c :=
  le_trans (le_max_left _ _) h

Left Element is Less Than or Equal to Upper Bound of Maximum

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, if the maximum of $a$ and $b$ is less than or equal to $c$, then $a$ is less than or equal to $c$.

le_of_max_le_right theorem

{a b c : α} (h : max a b ≤ c) : b ≤ c

Full source

theorem le_of_max_le_right {a b c : α} (h : max a b ≤ c) : b ≤ c :=
  le_trans (le_max_right _ _) h

Right Component of Maximum Inequality Implies Individual Inequality

Informal description

For any elements $a, b, c$ in a linearly ordered set $\alpha$, if the maximum of $a$ and $b$ is less than or equal to $c$, then $b$ is less than or equal to $c$.

instCommutativeMax instance

: Std.Commutative (α := α) max

Full source

instance instCommutativeMax : Std.Commutative (α := α) max where comm := max_comm

Commutativity of the Maximum Operation in Linear Orders

Informal description

For any linearly ordered set $\alpha$, the maximum operation $\max$ is commutative. That is, for any two elements $a, b \in \alpha$, we have $\max(a, b) = \max(b, a)$.

instAssociativeMax instance

: Std.Associative (α := α) max

Full source

instance instAssociativeMax : Std.Associative (α := α) max where assoc := max_assoc

Associativity of the Maximum Operation in Linear Orders

Informal description

The maximum operation $\max$ on a linearly ordered set $\alpha$ is associative. That is, for any elements $a, b, c \in \alpha$, we have $\max(a, \max(b, c)) = \max(\max(a, b), c)$.

instCommutativeMin instance

: Std.Commutative (α := α) min

Full source

instance instCommutativeMin : Std.Commutative (α := α) min where comm := min_comm

Commutativity of the Minimum Operation in Linear Orders

Informal description

For any linearly ordered set $\alpha$, the minimum operation $\min$ is commutative. That is, for any two elements $a, b \in \alpha$, we have $\min(a, b) = \min(b, a)$.

instAssociativeMin instance

: Std.Associative (α := α) min

Full source

instance instAssociativeMin : Std.Associative (α := α) min where assoc := min_assoc

Associativity of the Minimum Operation in Linear Orders

Informal description

The minimum operation $\min$ on a linearly ordered set $\alpha$ is associative. That is, for any elements $a, b, c \in \alpha$, we have $\min(a, \min(b, c)) = \min(\min(a, b), c)$.

max_left_commutative theorem

: LeftCommutative (max : α → α → α)

Full source

theorem max_left_commutative : LeftCommutative (max : α → α → α) := ⟨max_left_comm⟩

Left-Commutativity of Maximum Operation in Linear Orders

Informal description

For any linearly ordered type $\alpha$, the maximum operation $\max : \alpha \to \alpha \to \alpha$ is left-commutative. That is, for any elements $a, b, c \in \alpha$, we have $\max(a, \max(b, c)) = \max(b, \max(a, c))$.

min_left_commutative theorem

: LeftCommutative (min : α → α → α)

Full source

theorem min_left_commutative : LeftCommutative (min : α → α → α) := ⟨min_left_comm⟩

Left-Commutativity of the Minimum Operation

Informal description

For any linearly ordered set $\alpha$, the minimum operation $\min : \alpha \to \alpha \to \alpha$ is left-commutative. That is, for all $a, b, c \in \alpha$, we have $\min a (\min b c) = \min b (\min a c)$.

Tags