Nat.bit1_lt_bit0
theorem Nat.bit1_lt_bit0 : ∀ {n m : ℕ}, n < m → bit1 n < bit0 m
This theorem, `Nat.bit1_lt_bit0`, states that for all natural numbers `n` and `m`, if `n` is less than `m`, then `bit1 n` is less than `bit0 m`. Here, `bit1 n` and `bit0 m` can be understood as specific transformations of `n` and `m`: `bit1 n` is defined as `2n + 1` and `bit0 m` is defined as `2m`. So, in essence, this theorem is saying that if `n` is less than `m`, then `2n + 1` is less than `2m`.
More concisely: For all natural numbers `n` and `m`, if `n` < `m`, then `2n + 1` < `2m`.
|
Nat.strong_induction_on
theorem Nat.strong_induction_on : ∀ {p : ℕ → Prop} (n : ℕ), (∀ (n : ℕ), (∀ m < n, p m) → p n) → p n
This theorem is a statement about strong induction on natural numbers. For any property `p` that applies to natural numbers, given a natural number `n`, if it's true that for any natural number `n`, if `p` is true for all natural numbers less than `n` then `p` is true for `n`, then it follows that `p` is true for the given `n`. In simpler terms, it states that if a property holds for `0` and for each natural number it holds that if the property is true for all smaller numbers then it's true for this number, then the property is true for all natural numbers.
More concisely: If a property holds for 0 and is closed under the successor function, then it holds for all natural numbers. (Strong Induction Principle)
|
Nat.bit0_lt_bit1
theorem Nat.bit0_lt_bit1 : ∀ {n m : ℕ}, n ≤ m → bit0 n < bit1 m
This theorem states that for all natural numbers `n` and `m`, if `n` is less than or equal to `m`, then `bit0 n` is less than `bit1 m`. Here, `bit0 n` represents the result of adding `n` to itself (equivalent to 2n in mathematics), and `bit1 m` represents the result of adding `m` to itself and then adding one (equivalent to 2m + 1 in mathematics). Thus, the theorem essentially asserts that 2n is less than 2m + 1 whenever n is less than or equal to m.
More concisely: For all natural numbers n and m, if n <= m then 2*n < 2*m + 1.
|
Nat.bit1_eq_succ_bit0
theorem Nat.bit1_eq_succ_bit0 : ∀ (n : ℕ), bit1 n = (bit0 n).succ
The theorem `Nat.bit1_eq_succ_bit0` states that for all natural numbers `n`, the operation `bit1 n` is equivalent to the successor of `bit0 n`. Here, `bit1 n` represents the operation of doubling a number and adding one, while `bit0 n` simply doubles the number. The `Nat.succ` function increments a natural number by one, thus `Nat.succ (bit0 n)` doubles a number and then increments it by one. Therefore, the theorem shows that these two operations are fundamentally the same.
More concisely: The theorem asserts that for all natural numbers `n`, the operation `bit1 n` equal `Nat.succ (bit0 n)`, where `bit0 n` doubles `n` and `bit1 n` doubles `n` and adds one.
|
Nat.find_min'
theorem Nat.find_min' : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n) {m : ℕ}, p m → Nat.find H ≤ m := by
sorry
The theorem `Nat.find_min'` states that for any decidable predicate `p` on natural numbers, if there exists a natural number `n` such that `p n` holds, then for any natural number `m` where `p m` also holds, the smallest natural number satisfying `p` (found by `Nat.find`) is less than or equal to `m`. In other words, `Nat.find` will always return the minimum natural number satisfying the predicate `p`.
More concisely: If `p` is a decidable predicate on natural numbers such that there exists an `n` with `p(n)` holding, then for any other `m` with `p(m)` holding, `Nat.find p` is less than or equal to `m`.
|
Nat.find_min
theorem Nat.find_min : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n) {m : ℕ}, m < Nat.find H → ¬p m := by
sorry
The theorem `Nat.find_min` states that for any decidable predicate `p` on natural numbers, if there exists a natural number satisfying `p`, and `m` is any natural number that is strictly less than the smallest natural number satisfying `p` (as provided by the function `Nat.find`), then `m` does not satisfy `p`. In other words, `Nat.find` gives the smallest natural number satisfying the given predicate, and no natural number less than this satisfies the predicate.
More concisely: For any decidable predicate `p` on natural numbers, if there exists an `n` such that `p(n)` holds, then for all `m` with `0 < m < n`, it is false that `p(m)` holds.
|
Nat.find_spec
theorem Nat.find_spec : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (H : ∃ n, p n), p (Nat.find H)
The theorem `Nat.find_spec` states that for any predicate `p` on natural numbers (`ℕ`) that is decidable (`DecidablePred`), given the existence of at least one natural number `n` for which the predicate `p` holds true (`∃ n, p n`), the natural number returned by the `Nat.find` function with respect to `H` is also a number for which the predicate `p` holds true (`p (Nat.find H)`). In other words, `Nat.find` returns a natural number that satisfies the predicate `p`, if such a number exists.
More concisely: If `p` is a decidable predicate on natural numbers and there exists a natural number `n` such that `p(n)` holds, then `Nat.find` returns such an `n`.
|
Nat.bit1_inj
theorem Nat.bit1_inj : ∀ {n m : ℕ}, bit1 n = bit1 m → n = m
The theorem `Nat.bit1_inj` states that for all natural numbers `n` and `m`, if the "bit1" (which is defined as twice the input number plus one) of `n` is equal to the "bit1" of `m`, then `n` must be equal to `m`. In other words, the "bit1" function is injective (or one-to-one) over the natural numbers, meaning that it never maps different inputs to the same output.
More concisely: If two natural numbers have the same "bit1" (twice the number plus one), then they are equal.
|
Nat.bit0_inj
theorem Nat.bit0_inj : ∀ {n m : ℕ}, bit0 n = bit0 m → n = m
This theorem, `Nat.bit0_inj`, states that for any two natural numbers `n` and `m`, if the doubling of `n` is equal to the doubling of `m` (expressed as `bit0 n = bit0 m`), then `n` must be equal to `m`. This essentially asserts the injectivity of the `bit0` operation on natural numbers, meaning that different natural numbers map to different doubled values. In other words, no two distinct natural numbers will have the same doubled value.
More concisely: If for natural numbers `n` and `m`, `2 * n = 2 * m`, then `n = m`.
|