Nat.min_le_right
theorem Nat.min_le_right : ∀ (a b : ℕ), min a b ≤ b
This theorem states that for any two natural numbers `a` and `b`, the minimum of `a` and `b` is always less than or equal to `b`. In other words, no matter what two natural numbers you choose, the smaller one (or either one if they are equal) will never be greater than `b`.
More concisely: For all natural numbers `a` and `b`, `a ≤ b`.
|
Nat.min_comm
theorem Nat.min_comm : ∀ (a b : ℕ), min a b = min b a
This theorem states that the minimum operation over natural numbers is commutative. In other words, for any two natural numbers `a` and `b`, the minimum of `a` and `b` is the same as the minimum of `b` and `a`. This aligns with the intuitive concept of minimum, where the order of the two numbers doesn't affect the result.
More concisely: For all natural numbers `a` and `b`, `a minimun b` equals `b minimum a`.
|
Nat.le_max_left
theorem Nat.le_max_left : ∀ (a b : ℕ), a ≤ max a b
This theorem states that for any two natural numbers `a` and `b`, `a` is less than or equal to the maximum of `a` and `b`. In other words, regardless of the values of `a` and `b`, the maximum of the two numbers is always greater than or equal to `a`. This is a fundamental property of the maximum function that holds true for any pair of natural numbers.
More concisely: For all natural numbers `a` and `b`, `a` <= max a b.
|
Nat.min_le_left
theorem Nat.min_le_left : ∀ (a b : ℕ), min a b ≤ a
This theorem states that for all natural numbers `a` and `b`, the minimum of `a` and `b` is less than or equal to `a`. In other words, `a` is always greater than or equal to the smaller value between `a` and `b`. This makes intuitive sense because `a` must either be greater than `b`, equal to `b`, or be the smaller number itself.
More concisely: For all natural numbers `a` and `b`, `a ≤ a` and `a ≤ b` imply `b ≤ a`. (In other words, `min a b ≤ a`.)
|
Nat.min_eq_right
theorem Nat.min_eq_right : ∀ {a b : ℕ}, b ≤ a → min a b = b
This is a theorem about the minimum operation on natural numbers in Lean 4. It states that for any pair of natural numbers `a` and `b`, if `b` is less than or equal to `a`, then the minimum of `a` and `b` is `b`. This corresponds to the intuitive rule from mathematics that if one number is less than or equal to another, then the smaller number is the minimum of the two.
More concisely: For all natural numbers `a` and `b`, if `b` ≤ `a`, then `min a b` = `b`.
|
Nat.min_eq_left
theorem Nat.min_eq_left : ∀ {a b : ℕ}, a ≤ b → min a b = a
This theorem, `Nat.min_eq_left`, states that for any two natural numbers `a` and `b`, if `a` is less than or equal to `b`, then the minimum of `a` and `b` is `a`. The theorem is essentially describing one of the properties of the minimum function in the context of natural numbers.
More concisely: For all natural numbers `a` and `b`, if `a` ≤ `b`, then `min a b` = `a`.
|
Nat.max_comm
theorem Nat.max_comm : ∀ (a b : ℕ), max a b = max b a
This theorem states that for any two natural numbers `a` and `b`, the maximum of `a` and `b` is equal to the maximum of `b` and `a`. In other words, the operation of taking the maximum of two numbers is commutative over the set of natural numbers. This is similar to saying, for instance, that $3 \oplus 2 = 2 \oplus 3$ where $\oplus$ denotes the operation of taking the maximum.
More concisely: For all natural numbers `a` and `b`, `max a b` equals `max b a`.
|