Mathlib.Data.Rat.Cast.Order._auxLemma.2
theorem Mathlib.Data.Rat.Cast.Order._auxLemma.2 :
∀ {K : Type u_5} [inst : LinearOrderedField K] {m n : ℚ}, (↑m ≤ ↑n) = (m ≤ n)
This theorem states that, for any instance `K` of a linearly ordered field, and for any rational numbers `m` and `n`, the inequality `m` less than or equal to `n` in the field `K` holds true if and only if the inequality `m` less than or equal to `n` holds true in the set of rational numbers. Here, the `↑` symbol is used to denote the embedding of the rational numbers into the field `K`.
More concisely: For any linearly ordered field `K` and rational numbers `m` and `n`, `m ≤ n` holds in `K` if and only if `m ≤ n` holds in the rational numbers.
|
Rat.cast_lt
theorem Rat.cast_lt : ∀ {K : Type u_5} [inst : LinearOrderedField K] {m n : ℚ}, ↑m < ↑n ↔ m < n
This theorem states that for any linear ordered field `K` and any two rational numbers `m` and `n`, the cast of `m` to `K` is less than the cast of `n` to `K` if and only if `m` is less than `n`. In other words, the inequality relationship between `m` and `n` is preserved when they are both cast to elements of the field `K`.
More concisely: For any linear ordered field `K`, the cast of rational number `m` to `K` is less than the cast of rational number `n` to `K` if and only if `m` is less than `n`.
|
Rat.cast_abs
theorem Rat.cast_abs : ∀ {K : Type u_5} [inst : LinearOrderedField K] {q : ℚ}, ↑|q| = |↑q|
This theorem states that for any rational number `q` and any linear ordered field `K`, the absolute value of `q` after being cast to `K` is the same as the absolute value of `q` itself cast to `K`. In other words, the operation of taking the absolute value commutes with the operation of casting from the rationals to another field. This can be written in mathematical notation as `|cast(q)| = cast(|q|)`.
More concisely: For any rational number q and linear ordered field K, the absolute value of q after being cast to K equals the absolute value of q itself when cast to K, that is, |cast(q)| = cast(|q|).
|
Mathlib.Data.Rat.Cast.Order._auxLemma.3
theorem Mathlib.Data.Rat.Cast.Order._auxLemma.3 :
∀ {K : Type u_5} [inst : LinearOrderedField K] {m n : ℚ}, (↑m < ↑n) = (m < n)
This theorem states that for any type `K` that is a linearly ordered field, and any two rational numbers `m` and `n`, the inequality of their casted versions (i.e., the converted versions of `m` and `n` to type `K`) is equivalent to the inequality of `m` and `n` themselves. In simpler terms, this means that if `m` is less than `n` in the rational numbers, then the casted version of `m` is also less than the casted version of `n` in type `K`, and vice versa.
More concisely: For any linearly ordered field `K` and rational numbers `m` and `n`, `m < n` if and only if the cast `K m` is strictly less than `K n`.
|
Rat.cast_le
theorem Rat.cast_le : ∀ {K : Type u_5} [inst : LinearOrderedField K] {m n : ℚ}, ↑m ≤ ↑n ↔ m ≤ n
This theorem, `Rat.cast_le`, states that for any type `K` that has an instance of `LinearOrderedField`, and for any rational numbers `m` and `n`, the cast of `m` to `K` is less than or equal to the cast of `n` to `K` if and only if `m` is less than or equal to `n`. In simpler terms, it ensures that the order of two rational numbers is maintained when they are cast to any type that is a linear ordered field.
More concisely: For any linear ordered field K and rational numbers m and n, m ≤ n if and only if K.cast m ≤ K.cast n.
|
Rat.cast_nonneg
theorem Rat.cast_nonneg : ∀ {K : Type u_5} [inst : LinearOrderedField K] {n : ℚ}, 0 ≤ ↑n ↔ 0 ≤ n
This theorem states that for any type `K` which is a linear ordered field, and a given rational number `n`, the non-negative condition (greater or equal to zero) is preserved under the cast from the rational number to `K`. In other words, `n` is non-negative when expressed as a rational number if and only if it is also non-negative when cast to the type `K`.
More concisely: For any linear ordered field `K` and rational number `n`, `0 ≤ n` if and only if `0 ≤ (n : K)`.
|