Int.ofNat_lt_ofNat_of_lt
theorem Int.ofNat_lt_ofNat_of_lt : ∀ {n m : ℕ}, n < m → ↑n < ↑m
This theorem, `Int.ofNat_lt_ofNat_of_lt`, is an alias for the reverse direction of `Int.ofNat_lt`. It states that for any two natural numbers `n` and `m`, if `n` is less than `m` (`n < m`), then the integer representation of `n` is less than the integer representation of `m` (`↑n < ↑m`). In other words, the order relation `<` is preserved when natural numbers are mapped to integers.
More concisely: For all natural numbers `n` and `m`, if `n` is less than `m`, then `INT(n)` is less than `INT(m)`. (Here, `INT` denotes the function that maps natural numbers to their integer representations.)
|
Int.le_of_ofNat_le_ofNat
theorem Int.le_of_ofNat_le_ofNat : ∀ {m n : ℕ}, ↑m ≤ ↑n → m ≤ n
This theorem, `Int.le_of_ofNat_le_ofNat`, is an alias for the forward direction of `Int.ofNat_le`. It states that for any two natural numbers `m` and `n`, if the integer representation of `m` is less than or equal to the integer representation of `n`, then `m` is less than or equal to `n`. In other words, it translates a comparison from the domain of integers back to the domain of natural numbers.
More concisely: For all natural numbers m and n, if int m <= int n then m <= n.
|
Int.lt_of_ofNat_lt_ofNat
theorem Int.lt_of_ofNat_lt_ofNat : ∀ {n m : ℕ}, ↑n < ↑m → n < m
This theorem, `Int.lt_of_ofNat_lt_ofNat`, is an alias for the forward direction of the `Int.ofNat_lt` theorem. It states that for any two natural numbers `n` and `m`, if the integer representation of `n` is less than the integer representation of `m`, then `n` itself is less than `m`. In other words, it shows that the `<` relation is preserved when translating from the natural numbers to the integers.
More concisely: If `n` is a natural number and the integer representation of `n` is less than the integer representation of `m`, then `n` is less than `m`.
|
Int.ofNat_le_ofNat_of_le
theorem Int.ofNat_le_ofNat_of_le : ∀ {m n : ℕ}, m ≤ n → ↑m ≤ ↑n
This is essentially an alias of the reverse direction of the `Int.ofNat_le` theorem. It states that for any two natural numbers `m` and `n`, if `m` is less than or equal to `n`, then the integer representation of `m` is also less than or equal to the integer representation of `n`. In other words, the order of the numbers is maintained when they are converted from natural numbers to integers.
More concisely: If `m` is a natural number less than or equal to `n`, then `Int.fromNat m` is less than or equal to `Int.fromNat n`.
|