Nat.size_le
theorem Nat.size_le : ∀ {m n : ℕ}, m.size ≤ n ↔ m < 2 ^ n
This theorem, `Nat.size_le`, asserts that for any two natural numbers `m` and `n`, the size of `m` (i.e., the length of its binary representation) is less than or equal to `n` if and only if `m` is less than 2 to the power `n`. This theorem establishes a relationship between the size of a natural number in binary and the powers of 2, providing a way to compare natural numbers and their binary sizes.
More concisely: The size of a natural number in binary is less than or equal to the given natural number if and only if the number is less than 2 raised to the power of that number.
|
Nat.size_zero
theorem Nat.size_zero : Nat.size 0 = 0
The theorem `Nat.size_zero` asserts that the size of the natural number 0, in terms of its binary representation, is 0. In other words, the binary length of the number 0 is zero, which is intuitively true as 0 does not have any binary digits.
More concisely: The theorem `Nat.size_zero` asserts that the size of the natural number 0, in Lean's binary representation, is 0.
|
Nat.lt_size_self
theorem Nat.lt_size_self : ∀ (n : ℕ), n < 2 ^ n.size
This theorem states that, for any natural number 'n', 'n' is less than 2 raised to the power of the size of 'n'. Here, the size of 'n' refers to the length of its binary representation. In other words, any natural number is less than 2 to the power of the number of bits in its binary form.
More concisely: For all natural numbers n, the binary representation of n has length at most the log2 base 2 of n + 1, so 2^(log2 base 2 of n) ≤ n.
|
Nat.size_bit
theorem Nat.size_bit : ∀ {b : Bool} {n : ℕ}, Nat.bit b n ≠ 0 → (Nat.bit b n).size = n.size.succ
The theorem `Nat.size_bit` states that for any boolean `b` and natural number `n`, if the binary representation of `n` appended with the digit `b` (as performed by the function `Nat.bit b n`) is not zero, then the size (in bits) of this new number is exactly one more than the size of `n`. Here, the size of a number is defined as the length of its binary representation. This essentially means that appending a bit to the binary representation of a number increases its size by one, given that the resulting number is not zero.
More concisely: If the binary representation of a natural number `n` is appended with a bit `b`, resulting in a non-zero number, then the number of bits in the binary representation of the new number is one more than the number of bits in the binary representation of `n`.
|