Nat.nth_apply_eq_orderIsoOfNat
theorem Nat.nth_apply_eq_orderIsoOfNat :
∀ {p : ℕ → Prop} (hf : (setOf p).Infinite) (n : ℕ), Nat.nth p n = ↑((Nat.Subtype.orderIsoOfNat (setOf p)) n) := by
sorry
This theorem states that for any predicate `p` on natural numbers such that the set of natural numbers satisfying `p` is infinite, the `n`-th natural number satisfying `p` obtained using `Nat.nth` is the same as the `n`-th element of the order isomorphism between natural numbers and the subset satisfying `p` obtained using `Nat.Subtype.orderIsoOfNat`. In other words, when the set satisfying a certain condition is infinite, two different methods of enumerating elements from that set will yield the same natural number for the same index `n`.
More concisely: For an infinite predicate `p` on natural numbers, `Nat.nth (Nat.Subtype.orderIsoOfNat ^-<$> p) n = n-th element of the subset of natural numbers satisfying `p` for any `n`.
|
Nat.range_nth_of_infinite
theorem Nat.range_nth_of_infinite : ∀ {p : ℕ → Prop}, (setOf p).Infinite → Set.range (Nat.nth p) = setOf p
The theorem `Nat.range_nth_of_infinite` states that for any predicate `p` on natural numbers, if the set of natural numbers satisfying `p` is infinite, then the range of the function that maps each natural number to the corresponding `n`-th natural number satisfying `p` is exactly the set of all natural numbers satisfying `p`. In other words, if there are infinitely many natural numbers satisfying `p`, then every such natural number is the `n`-th satisfying `p` for some `n`.
More concisely: If a predicate `p` on natural numbers has an infinite number of solutions, then the function mapping each natural number to the `n`-th solution of `p` is a surjection from the set of natural numbers.
|
Nat.nth_strictMonoOn
theorem Nat.nth_strictMonoOn :
∀ {p : ℕ → Prop} (hf : (setOf p).Finite), StrictMonoOn (Nat.nth p) (Set.Iio hf.toFinset.card)
The theorem `Nat.nth_strictMonoOn` states that for any predicate `p` on natural numbers, if the set of natural numbers satisfying `p` is finite, then the function `Nat.nth p`, which returns the `n`-th natural number satisfying `p`, is strictly monotonic on the left-infinite right-open interval determined by the cardinality of the finset representation of the set. In simpler terms, if we take the set of all natural numbers that satisfy a certain condition and this set is finite, then as we look at the sequence of these numbers in increasing order, each number in sequence is smaller than the next one as long as we stay within the bounds defined by the size of this set.
More concisely: If a finite set of natural numbers is ordered by the natural numbers themselves, then the function returning the n-th element of the set is strictly increasing.
|
Nat.exists_lt_card_nth_eq
theorem Nat.exists_lt_card_nth_eq :
∀ {p : ℕ → Prop} {x : ℕ}, p x → ∃ n, (∀ (hf : (setOf p).Finite), n < hf.toFinset.card) ∧ Nat.nth p n = x
The theorem `Nat.exists_lt_card_nth_eq` states that for any predicate `p` on natural numbers and any natural number `x` that satisfies the predicate `p`, there exists a natural number `n` having two properties: first, for every finite set that represents the set of natural numbers satisfying `p`, the number `n` is less than the cardinality of that finite set; second, `n` is the index of `x` in the sequence of natural numbers satisfying `p`, where indexing starts from `0`. If `p` is true for an infinite number of natural numbers, the sequence is ordered using a canonical order isomorphism with the set of natural numbers.
More concisely: For any predicate `p` on natural numbers, if there exists a natural number `x` satisfying `p`, then there exists a natural number `n` less than the cardinality of the finite or infinite set of natural numbers satisfying `p` and equal to the index of `x` in that set (zero-indexed).
|
Nat.nth_eq_sInf
theorem Nat.nth_eq_sInf : ∀ (p : ℕ → Prop) (n : ℕ), Nat.nth p n = sInf {x | p x ∧ ∀ k < n, Nat.nth p k < x}
The theorem `Nat.nth_eq_sInf` provides an alternative recursive definition for the function `Nat.nth`. According to this theorem, for a given property `p` and a natural number `n`, the `n`-th natural number satisfying `p`, denoted as `Nat.nth p n`, is the greatest lower bound (infimum) of the set of natural numbers `x` that satisfy the property `p` and are greater than the `k`-th satisfying number for all `k` less than `n`. This holds true if the set is non-empty. However, we do not assume the set to be non-empty, and use the same default value `0` for both `sInf` on natural numbers and for `Nat.nth s n` when `n` is greater than or equal to the cardinality of the set `s`.
More concisely: The theorem `Nat.nth_eq_sInf` states that for any property `p` and natural number `n`, `Nat.nth p n` is the greatest lower bound of the set of natural numbers satisfying `p` and strictly greater than `Nat.nth p k` for all `k` less than `n`, or equal to 0 if this set is empty or has fewer elements than `n`.
|
Nat.filter_range_nth_eq_insert
theorem Nat.filter_range_nth_eq_insert :
∀ {p : ℕ → Prop} [inst : DecidablePred p] {k : ℕ},
(∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card) →
Finset.filter p (Finset.range (Nat.nth p (k + 1))) =
insert (Nat.nth p k) (Finset.filter p (Finset.range (Nat.nth p k)))
This theorem states that for any predicate `p` on natural numbers that is decidable, and for any natural number `k`, given that whenever the set of natural numbers satisfying the predicate `p` is finite, the number `k + 1` is strictly less than the size of the corresponding finite set. Then, the set of natural numbers less than the `(k + 1)`-th number that satisfies `p` and also satisfy `p` is equal to the set which is formed by adding the `k`-th number that satisfies `p` to the set of natural numbers less than the `k`-th number that satisfies `p` and also satisfy `p`. In other words, the set of the first `(k + 1)` numbers that satisfy `p` is obtained by adding the `(k + 1)`-th number that satisfies `p` to the set of the first `k` numbers that satisfy `p`.
More concisely: If `p` is a decidable predicate on natural numbers such that the set of numbers satisfying `p` is finite when it exists, then the first `(k + 1)` numbers in this finite set are those that can be obtained by adding the `(k + 1)`-th number in the set to the first `k` numbers in the set.
|
Nat.nth_strictMono
theorem Nat.nth_strictMono : ∀ {p : ℕ → Prop}, (setOf p).Infinite → StrictMono (Nat.nth p)
The theorem `Nat.nth_strictMono` states that for any predicate `p` on natural numbers, if the set of natural numbers satisfying `p` is infinite, then the function `Nat.nth p`, which returns the `n`-th natural number that satisfies `p`, is strictly monotone. This means that if `a < b`, then `Nat.nth p a < Nat.nth p b`. In essence, it says that as we increase `n`, the `n`-th natural number satisfying `p` also strictly increases, given an infinite set of natural numbers that satisfy `p`.
More concisely: If a predicate `p` on natural numbers defines an infinite set, then the function `Nat.nth p` is strictly increasing.
|
Nat.isLeast_nth
theorem Nat.isLeast_nth :
∀ {p : ℕ → Prop} {n : ℕ},
(∀ (hf : (setOf p).Finite), n < hf.toFinset.card) → IsLeast {i | p i ∧ ∀ k < n, Nat.nth p k < i} (Nat.nth p n)
The theorem `Nat.isLeast_nth` states that for any predicate `p` on natural numbers and for any natural number `n`, given that for every finite set built from `p`, the cardinality of the finite set is greater than `n`, then `Nat.nth p n` is a least element of the set `{i | p i ∧ ∀ k < n, Nat.nth p k < i}`. In other words, `Nat.nth p n` belongs to the set `{i | p i ∧ ∀ k < n, Nat.nth p k < i}` and it is smaller than or equal to all other elements in the set. Here, `Nat.nth p n` refers to the `n`-th natural number that satisfies predicate `p` (or `0` if no such number exists), and `{i | p i ∧ ∀ k < n, Nat.nth p k < i}` is the set of natural numbers which satisfy `p` and are greater than every natural number from the first to the `(n-1)`-th one that satisfies `p`.
More concisely: If for all finite sets built from a predicate `p` on natural numbers, the cardinality of the set of natural numbers satisfying `p` and strictly less than `n` is greater than `n`, then `Nat.nth p n` is the smallest natural number in the set `{i | p i ∧ ∀ k < n, Nat.i < i}`.
|
Nat.nth_eq_orderIsoOfNat
theorem Nat.nth_eq_orderIsoOfNat :
∀ {p : ℕ → Prop} (hf : (setOf p).Infinite), Nat.nth p = Subtype.val ∘ ⇑(Nat.Subtype.orderIsoOfNat (setOf p)) := by
sorry
This theorem states that for any predicate `p` on natural numbers, when the set of natural numbers satisfying `p` (denoted by `setOf p`) is infinite, the function `Nat.nth p`, which gives the `n`-th natural number satisfying `p`, is equivalent to the composition of `Subtype.val` and `Nat.Subtype.orderIsoOfNat (setOf p)`. Here, `Nat.Subtype.orderIsoOfNat (setOf p)` is an order isomorphism between the natural numbers and the set of natural numbers satisfying `p`, and `Subtype.val` returns the underlying element from a subtype. In other words, when dealing with an infinite set of natural numbers that satisfy a given predicate, the two methods for determining the `n`-th such number—either through `Nat.nth` or through the order isomorphism—yield the same result.
More concisely: For an infinite set of natural numbers satisfying a predicate `p`, the `n`-th element `Nat.nth p n` is equivalent to the underlying element `Subtype.val (Nat.Subtype.orderIsoOfNat (setOf p) !n)` obtained from the `n`-th element under the order isomorphism `Nat.Subtype.orderIsoOfNat (setOf p)`.
|
Nat.count_nth
theorem Nat.count_nth :
∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ},
(∀ (hf : (setOf p).Finite), n < hf.toFinset.card) → Nat.count p (Nat.nth p n) = n
The theorem `Nat.count_nth` states that for any decidable predicate `p` applied to natural numbers, and for any natural number `n`, if `n` is strictly less than the cardinality of the finite set derived from the predicate `p`, then the count of natural numbers less than the `n`-th natural number satisfying `p` equals `n` itself. In other words, it counts how many natural numbers below the `n`-th number satisfy the predicate `p` and asserts that this count is equal to `n`.
More concisely: For any decidable predicate `p` on natural numbers and `n` less than the cardinality of `{x | p x}`, the number of natural numbers `x` such that `x < n` and `p x` holds equals `n`.
|
Nat.nth_of_card_le
theorem Nat.nth_of_card_le : ∀ {p : ℕ → Prop} (hf : (setOf p).Finite) {n : ℕ}, hf.toFinset.card ≤ n → Nat.nth p n = 0
This theorem states that for any predicate `p` on natural numbers (`ℕ → Prop`), if the set of natural numbers satisfying `p` is finite (represented by the condition `Set.Finite (setOf p)`), then for any natural number `n`, if the cardinality of the finite set is less than or equal to `n` (represented by `(Set.Finite.toFinset hf).card ≤ n`), the `n`-th natural number satisfying `p` is `0`, represented by `Nat.nth p n = 0`. In other words, if you try to enumerate natural numbers satisfying `p` beyond the size of the set, you'll keep getting zeros.
More concisely: If a predicate `p` on natural numbers defines a finite set and the cardinality of this set is less than or equal to `n`, then the `n`-th natural number satisfying `p` is `0`.
|
Nat.nth_mem
theorem Nat.nth_mem : ∀ {p : ℕ → Prop} (n : ℕ), (∀ (hf : (setOf p).Finite), n < hf.toFinset.card) → p (Nat.nth p n)
The theorem `Nat.nth_mem` states that for any predicate `p` on natural numbers and any natural number `n`, if the set of natural numbers satisfying `p` is finite and `n` is less than the cardinality of that set (when converted into a `Finset`), then the `n`-th natural number that satisfies `p` (where indexing starts from 0) also satisfies `p`. In other words, it ensures that the `n`-th number in the ordered list of natural numbers (that satisfy the predicate `p`) is indeed a number that satisfies `p`.
More concisely: If `p` is a finite predicate on natural numbers and `n` is less than the cardinality of the set of natural numbers satisfying `p`, then the `n`-th natural number satisfying `p` also satisfies `p`.
|