Denumerable.raise'_sorted
theorem Denumerable.raise'_sorted :
∀ (l : List ℕ) (n : ℕ), List.Sorted (fun x x_1 => x < x_1) (Denumerable.raise' l n)
The theorem `Denumerable.raise'_sorted` states that for any list of natural numbers `l` and any natural number `n`, the function `raise'` will produce a strictly increasing sequence. In other words, when `raise'` is applied to a list of natural numbers and a natural number, it results in a list where each term `x` is strictly less than the following term `x_1`, demonstrating that the output is a list sorted in ascending order. The `raise'` function transforms the input list into a list of partial sums plus one, ensuring distinct elements.
More concisely: For any list of natural numbers and any natural number, the function `raise'` returns a strictly increasing list of their partial sums plus one.
|
Denumerable.raise_sorted
theorem Denumerable.raise_sorted : ∀ (l : List ℕ) (n : ℕ), List.Sorted (fun x x_1 => x ≤ x_1) (Denumerable.raise l n)
The theorem `Denumerable.raise_sorted` states that for any list of natural numbers `l` and a natural number `n`, the function `Denumerable.raise` generates a list that is non-decreasing. In other words, when `Denumerable.raise` is applied to `l` and `n` the resulting list is sorted such that every element at a position `i` in the list is less than or equal to the element at position `i+1`. The sorting is done according to the "less than or equal to" (`≤`) relation.
More concisely: For any list `l` of natural numbers and natural number `n`, the list `Denumerable.raise l n` is non-decreasing, i.e., for all `i`, the element at position `i` is less than or equal to the element at position `i+1` (`l.nth i ≤ l.nth (i+1)`).
|