Init.Data.Nat.MinMax

Nat.min_eq_min theorem

(a : Nat) : Nat.min a b = min a b

Full source

protected theorem min_eq_min (a : Nat) : Nat.min a b = min a b := rfl

Reflexivity of Minimum Operation on Natural Numbers

Informal description

For any natural numbers $a$ and $b$, the minimum operation defined on $\mathbb{N}$ satisfies $\min(a, b) = \min(a, b)$.

Nat.zero_min theorem

(a : Nat) : min 0 a = 0

Full source

@[simp] protected theorem zero_min (a : Nat) : min 0 a = 0 := by
  simp [Nat.min_def]

Minimum with Zero: $\min(0, a) = 0$

Informal description

For any natural number $a$, the minimum of $0$ and $a$ is equal to $0$.

Nat.min_zero theorem

(a : Nat) : min a 0 = 0

Full source

@[simp] protected theorem min_zero (a : Nat) : min a 0 = 0 := by
  simp [Nat.min_def]

Minimum with Zero: $\min(a, 0) = 0$ for natural numbers

Informal description

For any natural number $a$, the minimum of $a$ and $0$ is $0$, i.e., $\min(a, 0) = 0$.

Nat.add_min_add_right theorem

(a b c : Nat) : min (a + c) (b + c) = min a b + c

Full source

@[simp] protected theorem add_min_add_right (a b c : Nat) : min (a + c) (b + c) = min a b + c := by
  rw [Nat.min_def, Nat.min_def]
  simp only [Nat.add_le_add_iff_right]
  split <;> simp

Right Addition Preserves Minimum in Natural Numbers: $\min(a + c, b + c) = \min(a, b) + c$

Informal description

For any natural numbers $a$, $b$, and $c$, the minimum of $a + c$ and $b + c$ is equal to the minimum of $a$ and $b$ plus $c$, i.e., $\min(a + c, b + c) = \min(a, b) + c$.

Nat.add_min_add_left theorem

(a b c : Nat) : min (a + b) (a + c) = a + min b c

Full source

@[simp] protected theorem add_min_add_left (a b c : Nat) : min (a + b) (a + c) = a + min b c := by
  rw [Nat.min_def, Nat.min_def]
  simp only [Nat.add_le_add_iff_left]
  split <;> simp

Minimum Distributes Over Addition on the Left: $\min(a + b, a + c) = a + \min(b, c)$

Informal description

For any natural numbers $a, b, c$, the minimum of the sums $a + b$ and $a + c$ is equal to $a$ plus the minimum of $b$ and $c$, i.e., \[ \min(a + b, a + c) = a + \min(b, c). \]

Nat.mul_min_mul_right theorem

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

Full source

@[simp] protected theorem mul_min_mul_right (a b c : Nat) : min (a * c) (b * c) = min a b * c := by
  by_cases h : 0 < c
  · rw [Nat.min_def, Nat.min_def]
    simp only [Nat.mul_le_mul_right_iff h]
    split <;> simp
  · replace h : c = 0 := by exact Nat.eq_zero_of_not_pos h
    subst h
    simp

Right Multiplication Preserves Minimum in Natural Numbers: $\min(a \cdot c, b \cdot c) = \min(a, b) \cdot c$

Informal description

For any natural numbers $a$, $b$, and $c$, the minimum of the products $a \cdot c$ and $b \cdot c$ is equal to the minimum of $a$ and $b$ multiplied by $c$, i.e., \[ \min(a \cdot c, b \cdot c) = \min(a, b) \cdot c. \]

Nat.mul_min_mul_left theorem

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

Full source

@[simp] protected theorem mul_min_mul_left (a b c : Nat) : min (a * b) (a * c) = a * min b c := by
  rw [Nat.mul_comm a, Nat.mul_comm a, Nat.mul_min_mul_right, Nat.mul_comm]

Left Multiplication Preserves Minimum in Natural Numbers: $\min(a \cdot b, a \cdot c) = a \cdot \min(b, c)$

Informal description

For any natural numbers $a$, $b$, and $c$, the minimum of the products $a \cdot b$ and $a \cdot c$ is equal to $a$ multiplied by the minimum of $b$ and $c$, i.e., \[ \min(a \cdot b, a \cdot c) = a \cdot \min(b, c). \]

Nat.min_comm theorem

(a b : Nat) : min a b = min b a

Full source

protected theorem min_comm (a b : Nat) : min a b = min b a := by
  match Nat.lt_trichotomy a b with
  | .inl h => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]
  | .inr (.inl h) => simp [Nat.min_def, h]
  | .inr (.inr h) => simp [Nat.min_def, h, Nat.le_of_lt, Nat.not_le_of_lt]

Commutativity of Minimum Operation on Natural Numbers: $\min(a, b) = \min(b, a)$

Informal description

For any natural numbers $a$ and $b$, the minimum of $a$ and $b$ is equal to the minimum of $b$ and $a$, i.e., $\min(a, b) = \min(b, a)$.

Nat.instCommutativeMin instance

: Std.Commutative (α := Nat) min

Full source

instance : Std.Commutative (α := Nat) min := ⟨Nat.min_comm⟩

Commutativity of Minimum Operation on Natural Numbers

Informal description

The minimum operation $\min$ on natural numbers is commutative.

Nat.min_le_right theorem

(a b : Nat) : min a b ≤ b

Full source

protected theorem min_le_right (a b : Nat) : min a b ≤ b := by
  by_cases (a ≤ b) <;> simp [Nat.min_def, *]

Minimum is Less Than or Equal to Right Argument

Informal description

For any natural numbers $a$ and $b$, the minimum of $a$ and $b$ is less than or equal to $b$, i.e., $\min(a, b) \leq b$.

Nat.min_le_left theorem

(a b : Nat) : min a b ≤ a

Full source

protected theorem min_le_left (a b : Nat) : min a b ≤ a :=
  Nat.min_comm .. ▸ Nat.min_le_right ..

Minimum is Less Than or Equal to Left Argument

Informal description

For any natural numbers $a$ and $b$, the minimum of $a$ and $b$ is less than or equal to $a$, i.e., $\min(a, b) \leq a$.

Nat.min_eq_left theorem

{a b : Nat} (h : a ≤ b) : min a b = a

Full source

protected theorem min_eq_left {a b : Nat} (h : a ≤ b) : min a b = a := if_pos h

Minimum of Two Natural Numbers When First is Smaller

Informal description

For any natural numbers $a$ and $b$ such that $a \leq b$, the minimum of $a$ and $b$ equals $a$, i.e., $\min(a, b) = a$.

Nat.min_eq_right theorem

{a b : Nat} (h : b ≤ a) : min a b = b

Full source

protected theorem min_eq_right {a b : Nat} (h : b ≤ a) : min a b = b :=
  Nat.min_comm .. ▸ Nat.min_eq_left h

Minimum of Two Natural Numbers When Second is Smaller

Informal description

For any natural numbers $a$ and $b$ such that $b \leq a$, the minimum of $a$ and $b$ equals $b$, i.e., $\min(a, b) = b$.

Nat.le_min_of_le_of_le theorem

{a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c

Full source

protected theorem le_min_of_le_of_le {a b c : Nat} : a ≤ b → a ≤ c → a ≤ min b c := by
  intros; cases Nat.le_total b c with
  | inl h => rw [Nat.min_eq_left h]; assumption
  | inr h => rw [Nat.min_eq_right h]; assumption

Minimum Lower Bound: $a \leq \min(b, c)$ when $a \leq b$ and $a \leq c$

Informal description

For any natural numbers $a$, $b$, and $c$, if $a \leq b$ and $a \leq c$, then $a \leq \min(b, c)$.

Nat.le_min theorem

{a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

Full source

protected theorem le_min {a b c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c :=
  ⟨fun h => ⟨Nat.le_trans h (Nat.min_le_left ..), Nat.le_trans h (Nat.min_le_right ..)⟩,
   fun ⟨h₁, h₂⟩ => Nat.le_min_of_le_of_le h₁ h₂⟩

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

Informal description

For any natural numbers $a$, $b$, and $c$, the inequality $a \leq \min(b, c)$ holds if and only if both $a \leq b$ and $a \leq c$ hold.

Nat.lt_min theorem

{a b c : Nat} : a < min b c ↔ a < b ∧ a < c

Full source

protected theorem lt_min {a b c : Nat} : a < min b c ↔ a < b ∧ a < c := Nat.le_min

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

Informal description

For any natural numbers $a$, $b$, and $c$, the strict inequality $a < \min(b, c)$ holds if and only if both $a < b$ and $a < c$ hold.

Nat.max_eq_max theorem

(a : Nat) : Nat.max a b = max a b

Full source

protected theorem max_eq_max (a : Nat) : Nat.max a b = max a b := rfl

Equivalence of `Nat.max` and Mathematical Maximum

Informal description

For any natural number $a$, the maximum of $a$ and $b$ computed via `Nat.max` is equal to the maximum of $a$ and $b$ computed via the standard mathematical function $\max(a, b)$.

Nat.zero_max theorem

(a : Nat) : max 0 a = a

Full source

@[simp] protected theorem zero_max (a : Nat) : max 0 a = a := by
  simp [Nat.max_def]

Maximum with Zero: $\max(0, a) = a$

Informal description

For any natural number $a$, the maximum of $0$ and $a$ is equal to $a$, i.e., $\max(0, a) = a$.

Nat.max_zero theorem

(a : Nat) : max a 0 = a

Full source

@[simp] protected theorem max_zero (a : Nat) : max a 0 = a := by
  simp +contextual [Nat.max_def]

Maximum with Zero: $\max(a, 0) = a$

Informal description

For any natural number $a$, the maximum of $a$ and $0$ is equal to $a$, i.e., $\max(a, 0) = a$.

Nat.add_max_add_right theorem

(a b c : Nat) : max (a + c) (b + c) = max a b + c

Full source

@[simp] protected theorem add_max_add_right (a b c : Nat) : max (a + c) (b + c) = max a b + c := by
  rw [Nat.max_def, Nat.max_def]
  simp only [Nat.add_le_add_iff_right]
  split <;> simp

Right Addition Preserves Maximum in Natural Numbers: $\max(a + c, b + c) = \max(a, b) + c$

Informal description

For any natural numbers $a$, $b$, and $c$, the maximum of $a + c$ and $b + c$ is equal to the maximum of $a$ and $b$ plus $c$, i.e., $\max(a + c, b + c) = \max(a, b) + c$.

Nat.add_max_add_left theorem

(a b c : Nat) : max (a + b) (a + c) = a + max b c

Full source

@[simp] protected theorem add_max_add_left (a b c : Nat) : max (a + b) (a + c) = a + max b c := by
  rw [Nat.max_def, Nat.max_def]
  simp only [Nat.add_le_add_iff_left]
  split <;> simp

Left Additivity of Maximum: $\max(a + b, a + c) = a + \max(b, c)$

Informal description

For any natural numbers $a, b, c$, the maximum of $a + b$ and $a + c$ equals $a$ plus the maximum of $b$ and $c$, i.e., \[ \max(a + b, a + c) = a + \max(b, c). \]

Nat.mul_max_mul_right theorem

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

Full source

@[simp] protected theorem mul_max_mul_right (a b c : Nat) : max (a * c) (b * c) = max a b * c := by
  by_cases h : 0 < c
  · rw [Nat.max_def, Nat.max_def]
    simp only [Nat.mul_le_mul_right_iff h]
    split <;> simp
  · replace h : c = 0 := by exact Nat.eq_zero_of_not_pos h
    subst h
    simp

Right Multiplicativity of Maximum: $\max(a \cdot c, b \cdot c) = \max(a, b) \cdot c$

Informal description

For any natural numbers $a$, $b$, and $c$, the maximum of $a \cdot c$ and $b \cdot c$ equals the maximum of $a$ and $b$ multiplied by $c$, i.e., \[ \max(a \cdot c, b \cdot c) = \max(a, b) \cdot c. \]

Nat.mul_max_mul_left theorem

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

Full source

@[simp] protected theorem mul_max_mul_left (a b c : Nat) : max (a * b) (a * c) = a * max b c := by
  rw [Nat.mul_comm a, Nat.mul_comm a, Nat.mul_max_mul_right, Nat.mul_comm]

Left Multiplicativity of Maximum: $\max(a \cdot b, a \cdot c) = a \cdot \max(b, c)$

Informal description

For any natural numbers $a$, $b$, and $c$, the maximum of $a \cdot b$ and $a \cdot c$ equals $a$ multiplied by the maximum of $b$ and $c$, i.e., \[ \max(a \cdot b, a \cdot c) = a \cdot \max(b, c). \]

Nat.max_comm theorem

(a b : Nat) : max a b = max b a

Full source

protected theorem max_comm (a b : Nat) : max a b = max b a := by
  simp only [Nat.max_def]
  by_cases h₁ : a ≤ b <;> by_cases h₂ : b ≤ a <;> simp [h₁, h₂]
  · exact Nat.le_antisymm h₂ h₁
  · cases not_or_intro h₁ h₂ <| Nat.le_total ..

Commutativity of Maximum for Natural Numbers: $\max(a, b) = \max(b, a)$

Informal description

For any natural numbers $a$ and $b$, the maximum of $a$ and $b$ is equal to the maximum of $b$ and $a$, i.e., $\max(a, b) = \max(b, a)$.

Nat.instCommutativeMax instance

: Std.Commutative (α := Nat) max

Full source

instance : Std.Commutative (α := Nat) max := ⟨Nat.max_comm⟩

Commutativity of Maximum on Natural Numbers

Informal description

The maximum operation $\max$ on natural numbers is commutative.

Nat.le_max_left theorem

(a b : Nat) : a ≤ max a b

Full source

protected theorem le_max_left (a b : Nat) : a ≤ max a b := by
  by_cases (a ≤ b) <;> simp [Nat.max_def, *]

Left Argument is Less Than or Equal to Maximum

Informal description

For any natural numbers $a$ and $b$, the inequality $a \leq \max(a, b)$ holds.

Nat.le_max_right theorem

(a b : Nat) : b ≤ max a b

Full source

protected theorem le_max_right (a b : Nat) : b ≤ max a b :=
   Nat.max_comm .. ▸ Nat.le_max_left ..

Right Argument is Less Than or Equal to Maximum

Informal description

For any natural numbers $a$ and $b$, the inequality $b \leq \max(a, b)$ holds.

Nat.max_eq_right theorem

{a b : Nat} (h : a ≤ b) : max a b = b

Full source

protected theorem max_eq_right {a b : Nat} (h : a ≤ b) : max a b = b := if_pos h

Maximum of Two Natural Numbers When One is Less Than or Equal to the Other

Informal description

For any natural numbers $a$ and $b$ such that $a \leq b$, the maximum of $a$ and $b$ is equal to $b$, i.e., $\max(a, b) = b$.

Nat.max_eq_left theorem

{a b : Nat} (h : b ≤ a) : max a b = a

Full source

protected theorem max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a :=
  Nat.max_comm .. ▸ Nat.max_eq_right h

Maximum of Two Natural Numbers When One is Greater Than or Equal to the Other

Informal description

For any natural numbers $a$ and $b$ such that $b \leq a$, the maximum of $a$ and $b$ is equal to $a$, i.e., $\max(a, b) = a$.

Nat.max_le_of_le_of_le theorem

{a b c : Nat} : a ≤ c → b ≤ c → max a b ≤ c

Full source

protected theorem max_le_of_le_of_le {a b c : Nat} : a ≤ c → b ≤ c → max a b ≤ c := by
  intros; cases Nat.le_total a b with
  | inl h => rw [Nat.max_eq_right h]; assumption
  | inr h => rw [Nat.max_eq_left h]; assumption

Maximum of Two Natural Numbers is Bounded by a Common Upper Bound

Informal description

For any natural numbers $a$, $b$, and $c$, if $a \leq c$ and $b \leq c$, then $\max(a, b) \leq c$.

Nat.max_le theorem

{a b c : Nat} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

Full source

protected theorem max_le {a b c : Nat} : maxmax a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
  ⟨fun h => ⟨Nat.le_trans (Nat.le_max_left ..) h, Nat.le_trans (Nat.le_max_right ..) h⟩,
   fun ⟨h₁, h₂⟩ => Nat.max_le_of_le_of_le h₁ h₂⟩

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

Informal description

For any natural numbers $a$, $b$, and $c$, 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$ hold.

Nat.max_lt theorem

{a b c : Nat} : max a b < c ↔ a < c ∧ b < c

Full source

protected theorem max_lt {a b c : Nat} : maxmax a b < c ↔ a < c ∧ b < c :=
  match c with
  | 0 => by simp
  | c + 1 => by simpa [Nat.lt_add_one_iff] using Nat.max_le

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

Informal description

For any natural numbers $a$, $b$, and $c$, the maximum of $a$ and $b$ is strictly less than $c$ if and only if both $a < c$ and $b < c$ hold.