Nat.pair_unpair
theorem Nat.pair_unpair : ∀ (n : ℕ), n.unpair.1.pair n.unpair.2 = n
The theorem `Nat.pair_unpair` states that for all natural numbers `n`, if we first unpair `n` into a pair of natural numbers and then pair these numbers again using the defined pairing function `Nat.pair`, we will obtain the original number `n` back. In other words, the functions `Nat.pair` and `Nat.unpair` are inverses of each other with respect to this operation.
More concisely: For all natural numbers `n`, `Nat.pair (Nat.unpair n) = n` and `Nat.unpair (Nat.pair x y) = x + y`, where `x` and `y` are the components of the pair `Nat.pair x y`.
|
Nat.unpair_left_le
theorem Nat.unpair_left_le : ∀ (n : ℕ), n.unpair.1 ≤ n
This theorem states that for every natural number `n`, the first component of the pair obtained by unpairing `n` using the `Nat.unpair` function is always less than or equal to `n`. In other words, if we represent the unpaired values of `n` as a tuple `(a, b)`, then `a` is always less than or equal to `n` for all natural numbers `n`.
More concisely: For all natural numbers `n`, the first component of the unpaired representation `(a, _)` of `n` using `Nat.unpair` satisfies `a ≤ n`.
|
Nat.unpair_pair
theorem Nat.unpair_pair : ∀ (a b : ℕ), (a.pair b).unpair = (a, b)
The theorem `Nat.unpair_pair` states that for all natural numbers `a` and `b`, if you first pair them using the `Nat.pair` function and then unpair the result using the `Nat.unpair` function, you will get back the original pair `(a, b)`. In other words, the `Nat.unpair` function is the inverse of the `Nat.pair` function when applied to the result of the `Nat.pair` function. This is essentially a property of bijectiveness stating that every pair of natural numbers can be uniquely mapped to a single natural number and can be recovered from it.
More concisely: For all natural numbers `a` and `b`, `Nat.unpair (Nat.pair a b) = (a, b)`.
|
Nat.right_le_pair
theorem Nat.right_le_pair : ∀ (a b : ℕ), b ≤ a.pair b
The theorem `Nat.right_le_pair` states that for any two natural numbers `a` and `b`, `b` is always less than or equal to the value of the pairing function `Nat.pair a b`. In other words, when we apply the function `Nat.pair` on any two natural numbers `a` and `b`, the result will always be greater than or equal to `b`.
More concisely: For all natural numbers `a` and `b`, `Nat.pair a b` is greater than or equal to `b`.
|