Mathlib.Data.List.Intervals._auxLemma.3
theorem Mathlib.Data.List.Intervals._auxLemma.3 : ∀ {n m l : ℕ}, (l ∈ List.Ico n m) = (n ≤ l ∧ l < m)
This theorem states that for any three natural numbers `n`, `m`, and `l`, `l` is in the list `List.Ico n m` if and only if `n` is less than or equal to `l` and `l` is strictly less than `m`. In other words, `l` is a part of the list of natural numbers from `n` to `m`, excluding `m` (also known as the closed-open interval from `n` to `m`), precisely when `l` lies in the closed-open interval `[n, m)`.
More concisely: The natural number `l` is in the closed-open interval `[n, m)` (i.e., belongs to `List.Ico n m`) if and only if `n <= l` and `l < m`.
|
List.Ico.eq_nil_of_le
theorem List.Ico.eq_nil_of_le : ∀ {n m : ℕ}, m ≤ n → List.Ico n m = []
The theorem `List.Ico.eq_nil_of_le` states that for all natural numbers `n` and `m`, if `m` is less than or equal to `n`, then the interval from `n` to `m`, represented as a list of natural numbers where `n` is included and `m` is excluded (`List.Ico n m`), is an empty list. Essentially, there are no natural numbers `x` such that `n ≤ x < m` if `m ≤ n`.
More concisely: For all natural numbers n and m, the interval List.Ico n m is an empty list when m is less than or equal to n.
|
List.Ico.succ_singleton
theorem List.Ico.succ_singleton : ∀ {n : ℕ}, List.Ico n (n + 1) = [n]
This theorem states that for any natural number `n`, the list of natural numbers `n ≤ x < n + 1` (as defined by `List.Ico`) is a singleton list containing just the number `n`. In other words, when the interval is from `n` to `n+1`, the only natural number that lies within this interval is `n` itself.
More concisely: For any natural number `n`, the list of natural numbers `[n .. n+1]` (or `n ≤ x < n+1`) contains only the single element `n`.
|
List.Ico.append_consecutive
theorem List.Ico.append_consecutive : ∀ {n m l : ℕ}, n ≤ m → m ≤ l → List.Ico n m ++ List.Ico m l = List.Ico n l := by
sorry
The theorem `List.Ico.append_consecutive` states that for any natural numbers `n`, `m`, and `l`, if `n` is less than or equal to `m` and `m` is less than or equal to `l`, then the list of natural numbers from `n` to `m` (including `n` but excluding `m`), appended with the list of natural numbers from `m` to `l` (including `m` but excluding `l`), is equal to the list of natural numbers from `n` to `l` (including `n` but excluding `l`). This essentially means that we can concatenate two consecutive intervals to form a larger interval.
More concisely: For any natural numbers `n`, `m`, and `l` with `n ≤ m ≤ l`, the list of natural numbers from `n` to `m` followed by the list of natural numbers from `m` to `l` is equal to the list of natural numbers from `n` to `l`.
|
List.Ico.mem
theorem List.Ico.mem : ∀ {n m l : ℕ}, l ∈ List.Ico n m ↔ n ≤ l ∧ l < m
The theorem `List.Ico.mem` asserts that for any three natural numbers `n`, `m`, and `l`, `l` is a member of the interval list from `n` to `m` (denoted `List.Ico n m` in Lean) if and only if `l` is greater than or equal to `n` and less than `m`. In other words, `l` belongs to the closed-open interval `[n, m)` in the natural numbers. This theorem provides a condition for membership in this specific type of list of natural numbers in Lean.
More concisely: For any natural numbers n, m, and l, l belongs to the interval List.Ico n m if and only if n <= l < m.
|
Mathlib.Data.List.Intervals._auxLemma.7
theorem Mathlib.Data.List.Intervals._auxLemma.7 : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, (¬a < b) = (b ≤ a)
This theorem, `Mathlib.Data.List.Intervals._auxLemma.7`, states that for any type `α` that has a linear order, and for any two elements of this type `a` and `b`, the assertion that `a` is not less than `b` (`¬a < b`) is equivalent to the assertion that `b` is less than or equal to `a` (`b ≤ a`). This is a fundamental property of ordered types in mathematics, reflecting the relationship between inequality and order.
More concisely: For any type `α` with a linear order, the negation of `a < b` is equivalent to `b ≤ a`.
|
List.Ico.trichotomy
theorem List.Ico.trichotomy : ∀ (n a b : ℕ), n < a ∨ b ≤ n ∨ n ∈ List.Ico a b
For any natural numbers `n`, `a`, and `b`, this theorem states that one of the following conditions must be true: either `n` is less than `a`, `n` is greater than or equal to `b`, or `n` is in the list of natural numbers ranging from `a` (inclusive) to `b` (exclusive). In other words, `n` either falls before the interval, within the interval, or after the interval formed by `a` and `b`.
More concisely: For any natural numbers `n`, `a`, and `b`, either `n < a`, `n >= b`, or `a <= n < b`.
|