Mathlib.Data.Rat.Cast.Order

Rat.castHom_rat theorem

: castHom ℚ = RingHom.id ℚ

Full source

@[simp]
theorem castHom_rat : castHom ℚ = RingHom.id ℚ :=
  RingHom.ext cast_id

Identity Property of Rational Number Cast Homomorphism

Informal description

The canonical ring homomorphism from the rational numbers $\mathbb{Q}$ to itself is equal to the identity ring homomorphism on $\mathbb{Q}$.

Rat.cast_pos_of_pos theorem

(hq : 0 < q) : (0 : K) < q

Full source

theorem cast_pos_of_pos (hq : 0 < q) : (0 : K) < q := by
  rw [Rat.cast_def]
  exact div_pos (Int.cast_pos.2 <| num_pos.2 hq) (Nat.cast_pos.2 q.pos)

Positivity Preservation of Rational Embedding in Ordered Fields

Informal description

For any positive rational number $q > 0$ and any linear ordered field $K$, the canonical embedding of $q$ into $K$ is positive, i.e., $0 < q$ in $K$.

Rat.cast_strictMono theorem

: StrictMono ((↑) : ℚ → K)

Full source

@[mono]
theorem cast_strictMono : StrictMono ((↑) : ℚ → K) := fun p q => by
  simpa only [sub_pos, cast_sub] using cast_pos_of_pos (K := K) (q := q - p)

Strict Monotonicity of Rational Number Embedding in Ordered Fields

Informal description

The canonical embedding from the rational numbers $\mathbb{Q}$ to a linear ordered field $K$ is strictly monotone. That is, for any rational numbers $q_1, q_2 \in \mathbb{Q}$, if $q_1 < q_2$, then $q_1 < q_2$ in $K$.

Rat.cast_mono theorem

: Monotone ((↑) : ℚ → K)

Full source

@[mono]
theorem cast_mono : Monotone ((↑) : ℚ → K) :=
  cast_strictMono.monotone

Monotonicity of Rational Number Embedding in Ordered Fields

Informal description

The canonical embedding from the rational numbers $\mathbb{Q}$ to a linear ordered field $K$ is monotone. That is, for any rational numbers $q_1, q_2 \in \mathbb{Q}$, if $q_1 \leq q_2$, then $q_1 \leq q_2$ in $K$.

Rat.castOrderEmbedding definition

: ℚ ↪o K

Full source

/-- Coercion from `ℚ` as an order embedding. -/
@[simps!]
def castOrderEmbedding : ℚℚ ↪o K :=
  OrderEmbedding.ofStrictMono (↑) cast_strictMono

Order embedding of rational numbers into a linear ordered field

Informal description

The order embedding from the rational numbers $\mathbb{Q}$ to a linear ordered field $K$ is defined by the canonical embedding function, which is strictly monotone. That is, for any rational numbers $q_1, q_2 \in \mathbb{Q}$, if $q_1 < q_2$, then $q_1 < q_2$ in $K$.

Rat.cast_le theorem

: (p : K) ≤ q ↔ p ≤ q

Full source

@[simp, norm_cast] lemma cast_le : (p : K) ≤ q ↔ p ≤ q := castOrderEmbedding.le_iff_le

Order Preservation in Rational Number Cast: $(p : K) \leq (q : K) \leftrightarrow p \leq q$

Informal description

For any rational numbers $p, q \in \mathbb{Q}$ and any linear ordered field $K$, the canonical embedding satisfies $(p : K) \leq (q : K)$ if and only if $p \leq q$ in $\mathbb{Q}$.

Rat.cast_lt theorem

: (p : K) < q ↔ p < q

Full source

@[simp, norm_cast] lemma cast_lt : (p : K) < q ↔ p < q := cast_strictMono.lt_iff_lt

Order Preservation in Rational Number Cast: $(p : K) < (q : K) \leftrightarrow p < q$

Informal description

For any rational numbers $p, q \in \mathbb{Q}$ and any linear ordered field $K$, the canonical embedding satisfies $(p : K) < (q : K)$ if and only if $p < q$ in $\mathbb{Q}$.

Rat.cast_nonneg theorem

: 0 ≤ (q : K) ↔ 0 ≤ q

Full source

@[simp] lemma cast_nonneg : 0 ≤ (q : K) ↔ 0 ≤ q := by norm_cast

Nonnegativity Preservation in Rational Number Cast: $0 \leq (q : K) \leftrightarrow 0 \leq q$

Informal description

For any rational number $q$ and any linear ordered field $K$, the canonical injection of $q$ into $K$ satisfies $0 \leq (q : K)$ if and only if $0 \leq q$.

Rat.cast_nonpos theorem

: (q : K) ≤ 0 ↔ q ≤ 0

Full source

@[simp] lemma cast_nonpos : (q : K) ≤ 0 ↔ q ≤ 0 := by norm_cast

Nonpositivity Preservation in Rational Number Cast: $(q : K) \leq 0 \leftrightarrow q \leq 0$

Informal description

For any rational number $q$ and any linear ordered field $K$, the canonical injection of $q$ into $K$ satisfies $(q : K) \leq 0$ if and only if $q \leq 0$.

Rat.cast_pos theorem

: (0 : K) < q ↔ 0 < q

Full source

@[simp] lemma cast_pos : (0 : K) < q ↔ 0 < q := by norm_cast

Positivity Preservation in Rational Number Cast: $0 < (q : K) \leftrightarrow 0 < q$

Informal description

For any rational number $q$ and any linear ordered field $K$, the canonical injection of $q$ into $K$ satisfies $0 < (q : K)$ if and only if $0 < q$.

Rat.cast_lt_zero theorem

: (q : K) < 0 ↔ q < 0

Full source

@[simp] lemma cast_lt_zero : (q : K) < 0 ↔ q < 0 := by norm_cast

Strict Negativity Preservation in Rational Number Cast: $(q : K) < 0 \leftrightarrow q < 0$

Informal description

For any rational number $q$ and any linear ordered field $K$, the canonical injection of $q$ into $K$ satisfies $(q : K) < 0$ if and only if $q < 0$.

Rat.cast_le_natCast theorem

{m : ℚ} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ)

Full source

@[simp, norm_cast]
theorem cast_le_natCast {m : ℚ} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by
  rw [← cast_le (K := K), cast_natCast]

Inequality Preservation for Rational and Natural Number Casts: $(m : K) \leq n \leftrightarrow m \leq (n : \mathbb{Q})$

Informal description

For any rational number $m$, any natural number $n$, and any linear ordered field $K$, the inequality $(m : K) \leq n$ holds if and only if $m \leq (n : \mathbb{Q})$.

Rat.natCast_le_cast theorem

{m : ℕ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n

Full source

@[simp, norm_cast]
theorem natCast_le_cast {m : ℕ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n := by
  rw [← cast_le (K := K), cast_natCast]

Order Preservation of Natural Number Casts into Linear Ordered Fields: $(m : K) \leq n \leftrightarrow (m : \mathbb{Q}) \leq n$

Informal description

For any natural number $m$ and rational number $n$, and for any linear ordered field $K$, the canonical embedding satisfies $(m : K) \leq n$ if and only if $(m : \mathbb{Q}) \leq n$.

Rat.cast_le_intCast theorem

{m : ℚ} {n : ℤ} : (m : K) ≤ n ↔ m ≤ (n : ℚ)

Full source

@[simp, norm_cast]
theorem cast_le_intCast {m : ℚ} {n : ℤ} : (m : K) ≤ n ↔ m ≤ (n : ℚ) := by
  rw [← cast_le (K := K), cast_intCast]

Order Preservation of Rational Cast Against Integers: $(m : K) \leq n \leftrightarrow m \leq (n : \mathbb{Q})$

Informal description

For any rational number $m \in \mathbb{Q}$, any integer $n \in \mathbb{Z}$, and any linear ordered field $K$, the canonical embedding satisfies $(m : K) \leq n$ if and only if $m \leq (n : \mathbb{Q})$.

Rat.intCast_le_cast theorem

{m : ℤ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n

Full source

@[simp, norm_cast]
theorem intCast_le_cast {m : ℤ} {n : ℚ} : (m : K) ≤ n ↔ (m : ℚ) ≤ n := by
  rw [← cast_le (K := K), cast_intCast]

Order Comparison of Integer Cast and Rational Number in Linear Ordered Field: $(m : K) \leq n \leftrightarrow (m : \mathbb{Q}) \leq n$

Informal description

For any integer $m$, any rational number $n$, and any linear ordered field $K$, the inequality $(m : K) \leq n$ holds if and only if $(m : \mathbb{Q}) \leq n$ holds in $\mathbb{Q}$.

Rat.cast_lt_natCast theorem

{m : ℚ} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ)

Full source

@[simp, norm_cast]
theorem cast_lt_natCast {m : ℚ} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ) := by
  rw [← cast_lt (K := K), cast_natCast]

Order Preservation of Rational Cast Against Natural Numbers: $(m : K) < n \leftrightarrow m < (n : \mathbb{Q})$

Informal description

For any rational number $m \in \mathbb{Q}$, any natural number $n \in \mathbb{N}$, and any linear ordered field $K$, the canonical embedding satisfies $(m : K) < n$ if and only if $m < (n : \mathbb{Q})$.

Rat.natCast_lt_cast theorem

{m : ℕ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n

Full source

@[simp, norm_cast]
theorem natCast_lt_cast {m : ℕ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n := by
  rw [← cast_lt (K := K), cast_natCast]

Order Comparison of Natural Number Cast and Rational Number in Linear Ordered Field: $(m : K) < n \leftrightarrow (m : \mathbb{Q}) < n$

Informal description

For any natural number $m$ and rational number $n$, and for any linear ordered field $K$, the inequality $(m : K) < n$ holds if and only if $(m : \mathbb{Q}) < n$ holds in $\mathbb{Q}$.

Rat.cast_lt_intCast theorem

{m : ℚ} {n : ℤ} : (m : K) < n ↔ m < (n : ℚ)

Full source

@[simp, norm_cast]
theorem cast_lt_intCast {m : ℚ} {n : ℤ} : (m : K) < n ↔ m < (n : ℚ) := by
  rw [← cast_lt (K := K), cast_intCast]

Order Comparison of Rational Cast with Integer in Linear Ordered Field: $(m : K) < n \leftrightarrow m < (n : \mathbb{Q})$

Informal description

For any rational number $m$ and any integer $n$, the canonical embedding of $m$ into a linear ordered field $K$ satisfies $(m : K) < n$ if and only if $m < (n : \mathbb{Q})$.

Rat.intCast_lt_cast theorem

{m : ℤ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n

Full source

@[simp, norm_cast]
theorem intCast_lt_cast {m : ℤ} {n : ℚ} : (m : K) < n ↔ (m : ℚ) < n := by
  rw [← cast_lt (K := K), cast_intCast]

Order Preservation of Integer-to-Field Cast vs Rational Comparison: $(m : K) < n \leftrightarrow (m : \mathbb{Q}) < n$

Informal description

For any integer $m$ and rational number $n$, and for any linear ordered field $K$, the inequality $(m : K) < n$ holds if and only if $(m : \mathbb{Q}) < n$ in the rational numbers.

Rat.cast_min theorem

(p q : ℚ) : (↑(min p q) : K) = min (p : K) (q : K)

Full source

@[simp, norm_cast]
lemma cast_min (p q : ℚ) : (↑(min p q) : K) = min (p : K) (q : K) := (@cast_mono K _).map_min

Minimum Preservation under Rational Embedding in Ordered Fields

Informal description

For any rational numbers $p$ and $q$, the canonical embedding of their minimum into a linear ordered field $K$ is equal to the minimum of their embeddings, i.e., $\min(p, q) = \min(p, q)$ in $K$.

Rat.cast_max theorem

(p q : ℚ) : (↑(max p q) : K) = max (p : K) (q : K)

Full source

@[simp, norm_cast]
lemma cast_max (p q : ℚ) : (↑(max p q) : K) = max (p : K) (q : K) := (@cast_mono K _).map_max

Preservation of Maximum under Rational Embedding in Ordered Fields

Informal description

For any rational numbers $p$ and $q$, the canonical embedding of their maximum $\max(p, q)$ into a linear ordered field $K$ is equal to the maximum of their embeddings, i.e., $\max(p, q) = \max(p, q)$ in $K$.

Rat.cast_abs theorem

(q : ℚ) : ((|q| : ℚ) : K) = |(q : K)|

Full source

@[simp, norm_cast] lemma cast_abs (q : ℚ) : ((|q| : ℚ) : K) = |(q : K)| := by simp [abs_eq_max_neg]

Absolute Value Commutes with Rational Number Casting

Informal description

For any rational number $q$, the canonical embedding of the absolute value $|q|$ into a linear ordered field $K$ is equal to the absolute value of the embedding of $q$ in $K$, i.e., $(|q| : K) = |(q : K)|$.

Rat.preimage_cast_Icc theorem

(p q : ℚ) : (↑) ⁻¹' Icc (p : K) q = Icc p q

Full source

@[simp]
theorem preimage_cast_Icc (p q : ℚ) : (↑) ⁻¹' Icc (p : K) q = Icc p q :=
  castOrderEmbedding.preimage_Icc ..

Preimage of Closed Interval under Rational Embedding into Ordered Field

Informal description

For any rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the closed interval $[p, q]$ in the linear ordered field $K$ is equal to the closed interval $[p, q]$ in $\mathbb{Q}$. That is, $$ (\uparrow)^{-1}\big([p, q]\big) = [p, q]. $$

Rat.preimage_cast_Ico theorem

(p q : ℚ) : (↑) ⁻¹' Ico (p : K) q = Ico p q

Full source

@[simp]
theorem preimage_cast_Ico (p q : ℚ) : (↑) ⁻¹' Ico (p : K) q = Ico p q :=
  castOrderEmbedding.preimage_Ico ..

Preimage of Closed-Open Interval under Rational Embedding

Informal description

For any rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the closed-open interval $[p, q)$ in the linear ordered field $K$ is equal to the closed-open interval $[p, q)$ in $\mathbb{Q}$. That is, $$ (\uparrow)^{-1}\big([p, q)\big) = [p, q). $$

Rat.preimage_cast_Ioc theorem

(p q : ℚ) : (↑) ⁻¹' Ioc (p : K) q = Ioc p q

Full source

@[simp]
theorem preimage_cast_Ioc (p q : ℚ) : (↑) ⁻¹' Ioc (p : K) q = Ioc p q :=
  castOrderEmbedding.preimage_Ioc p q

Preimage of Open-Closed Interval under Rational Embedding into Ordered Field

Informal description

For any rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the open-closed interval $(p, q]$ in the linear ordered field $K$ is equal to the open-closed interval $(p, q]$ in $\mathbb{Q}$. That is, $$ \left( \mathbb{Q} \hookrightarrow K \right)^{-1}\big((p, q]\big) = (p, q]. $$

Rat.preimage_cast_Ioo theorem

(p q : ℚ) : (↑) ⁻¹' Ioo (p : K) q = Ioo p q

Full source

@[simp]
theorem preimage_cast_Ioo (p q : ℚ) : (↑) ⁻¹' Ioo (p : K) q = Ioo p q :=
  castOrderEmbedding.preimage_Ioo p q

Preimage of Open Interval under Rational Embedding

Informal description

For any rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the open interval $(p, q)$ in the linear ordered field $K$ is equal to the open interval $(p, q)$ in $\mathbb{Q}$. That is, $$ (\uparrow)^{-1}\big((p, q)\big) = (p, q). $$

Rat.preimage_cast_Ici theorem

(q : ℚ) : (↑) ⁻¹' Ici (q : K) = Ici q

Full source

@[simp]
theorem preimage_cast_Ici (q : ℚ) : (↑) ⁻¹' Ici (q : K) = Ici q :=
  castOrderEmbedding.preimage_Ici q

Preimage of Closed Right-Infinite Interval under Rational Embedding

Informal description

For any rational number $q \in \mathbb{Q}$ and any linear ordered field $K$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the closed right-infinite interval $[q, \infty)$ in $K$ is equal to the closed right-infinite interval $[q, \infty)$ in $\mathbb{Q}$, i.e., $$ (\uparrow)^{-1}\big([q, \infty)\big) = [q, \infty). $$

Rat.preimage_cast_Iic theorem

(q : ℚ) : (↑) ⁻¹' Iic (q : K) = Iic q

Full source

@[simp]
theorem preimage_cast_Iic (q : ℚ) : (↑) ⁻¹' Iic (q : K) = Iic q :=
  castOrderEmbedding.preimage_Iic q

Preimage of Closed Left-Infinite Interval under Rational Embedding

Informal description

For any rational number $q$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the closed left-infinite interval $(-\infty, q]$ in the linear ordered field $K$ is equal to the closed left-infinite interval $(-\infty, q]$ in $\mathbb{Q}$, i.e., $$ (\uparrow)^{-1}\big((-\infty, q]\big) = (-\infty, q]. $$

Rat.preimage_cast_Ioi theorem

(q : ℚ) : (↑) ⁻¹' Ioi (q : K) = Ioi q

Full source

@[simp]
theorem preimage_cast_Ioi (q : ℚ) : (↑) ⁻¹' Ioi (q : K) = Ioi q :=
  castOrderEmbedding.preimage_Ioi q

Preimage of Strict Right-Infinite Interval under Rational Embedding

Informal description

For any rational number $q \in \mathbb{Q}$ and any linear ordered field $K$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the strict right-infinite interval $(q, \infty)$ in $K$ is equal to the strict right-infinite interval $(q, \infty)$ in $\mathbb{Q}$, i.e., $$ (\uparrow)^{-1}\big((q, \infty)\big) = (q, \infty). $$

Rat.preimage_cast_Iio theorem

(q : ℚ) : (↑) ⁻¹' Iio (q : K) = Iio q

Full source

@[simp]
theorem preimage_cast_Iio (q : ℚ) : (↑) ⁻¹' Iio (q : K) = Iio q :=
  castOrderEmbedding.preimage_Iio q

Preimage of Strict Left-Infinite Interval under Rational Embedding

Informal description

For any rational number $q$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the strict left-infinite interval $(-\infty, q)$ in the linear ordered field $K$ is equal to the strict left-infinite interval $(-\infty, q)$ in $\mathbb{Q}$, i.e., $$ (\uparrow)^{-1}\big((-\infty, q)\big) = (-\infty, q). $$

Rat.preimage_cast_uIcc theorem

(p q : ℚ) : (↑) ⁻¹' uIcc (p : K) q = uIcc p q

Full source

@[simp]
theorem preimage_cast_uIcc (p q : ℚ) : (↑) ⁻¹' uIcc (p : K) q = uIcc p q :=
  (castOrderEmbedding (K := K)).preimage_uIcc p q

Preimage of Rational Embedding Preserves Unordered Closed Interval

Informal description

For any rational numbers $p, q \in \mathbb{Q}$ and any linear ordered field $K$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the unordered closed interval $[p \sqcap q, p \sqcup q]$ in $K$ is equal to the unordered closed interval $[p \sqcap q, p \sqcup q]$ in $\mathbb{Q}$. That is, $$ (\uparrow)^{-1}\big([\min(p, q), \max(p, q)]_K\big) = [\min(p, q), \max(p, q)]_{\mathbb{Q}}. $$

Rat.preimage_cast_uIoc theorem

(p q : ℚ) : (↑) ⁻¹' uIoc (p : K) q = uIoc p q

Full source

@[simp]
theorem preimage_cast_uIoc (p q : ℚ) : (↑) ⁻¹' uIoc (p : K) q = uIoc p q :=
  (castOrderEmbedding (K := K)).preimage_uIoc p q

Preimage of Generalized Open-Closed Interval under Rational Embedding into Ordered Field

Informal description

Let $K$ be a linearly ordered field. For any rational numbers $p, q \in \mathbb{Q}$, the preimage under the canonical embedding $\mathbb{Q} \hookrightarrow K$ of the generalized open-closed interval $\text{uIoc}(p, q)$ in $K$ equals the interval $\text{uIoc}(p, q)$ in $\mathbb{Q}$. That is, $$ (\mathbb{Q} \hookrightarrow K)^{-1}\big((\min(p, q), \max(p, q)]\big) = (\min(p, q), \max(p, q)]. $$

NNRat.cast_strictMono theorem

: StrictMono ((↑) : ℚ≥0 → K)

Full source

theorem cast_strictMono : StrictMono ((↑) : ℚ≥0 → K) := fun p q h => by
  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff₀, ← Nat.cast_mul, ← Nat.cast_mul,
    Nat.cast_lt (α := K), ← NNRat.lt_def]
  · simp
  · simp

Strict Monotonicity of Nonnegative Rational Embedding into Ordered Field

Informal description

The canonical embedding from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to a linearly ordered field $K$ is strictly monotone. That is, for any $x, y \in \mathbb{Q}_{\geq 0}$, if $x < y$ then their images in $K$ satisfy $x < y$.

NNRat.cast_mono theorem

: Monotone ((↑) : ℚ≥0 → K)

Full source

@[mono]
theorem cast_mono : Monotone ((↑) : ℚ≥0 → K) :=
  cast_strictMono.monotone

Monotonicity of Nonnegative Rational Embedding into Ordered Field

Informal description

The canonical embedding from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to a linearly ordered field $K$ is monotone. That is, for any $x, y \in \mathbb{Q}_{\geq 0}$, if $x \leq y$ then their images in $K$ satisfy $x \leq y$.

NNRat.castOrderEmbedding definition

: ℚ≥0 ↪o K

Full source

/-- Coercion from `ℚ` as an order embedding. -/
@[simps!]
def castOrderEmbedding : ℚ≥0ℚ≥0 ↪o K :=
  OrderEmbedding.ofStrictMono (↑) cast_strictMono

Order embedding of nonnegative rationals into a linearly ordered field

Informal description

The order embedding from the nonnegative rational numbers $\mathbb{Q}_{\geq 0}$ to a linearly ordered field $K$ is given by the canonical embedding function, which is strictly monotone. This means that for any $x, y \in \mathbb{Q}_{\geq 0}$, if $x < y$ then their images in $K$ satisfy $x < y$.

NNRat.cast_le theorem

: (p : K) ≤ q ↔ p ≤ q

Full source

@[simp, norm_cast] lemma cast_le : (p : K) ≤ q ↔ p ≤ q := castOrderEmbedding.le_iff_le

Nonnegative Rational Cast Preserves Order: $(p : K) \leq (q : K) \leftrightarrow p \leq q$

Informal description

For any nonnegative rational numbers $p, q \in \mathbb{Q}_{\geq 0}$ and any linearly ordered field $K$, the canonical embedding satisfies $(p : K) \leq (q : K)$ if and only if $p \leq q$.

NNRat.cast_lt theorem

: (p : K) < q ↔ p < q

Full source

@[simp, norm_cast] lemma cast_lt : (p : K) < q ↔ p < q := cast_strictMono.lt_iff_lt

Nonnegative Rational Cast Preserves Strict Order: $(p : K) < (q : K) \leftrightarrow p < q$

Informal description

For any nonnegative rational numbers $p, q \in \mathbb{Q}_{\geq 0}$ and any linearly ordered field $K$, the canonical embedding satisfies $(p : K) < (q : K)$ if and only if $p < q$.

NNRat.cast_nonpos theorem

: (q : K) ≤ 0 ↔ q ≤ 0

Full source

@[simp] lemma cast_nonpos : (q : K) ≤ 0 ↔ q ≤ 0 := by norm_cast

Non-Negative Rational Cast Preserves Non-Positivity: $(q : K) \leq 0 \leftrightarrow q \leq 0$

Informal description

For any non-negative rational number $q$ and any linear ordered field $K$, the canonical injection satisfies $(q : K) \leq 0$ if and only if $q \leq 0$.

NNRat.cast_pos theorem

: (0 : K) < q ↔ 0 < q

Full source

@[simp] lemma cast_pos : (0 : K) < q ↔ 0 < q := by norm_cast

Non-Negative Rational Cast Preserves Positivity: $(0 : K) < q \leftrightarrow 0 < q$

Informal description

For any non-negative rational number $q$ and any linear ordered field $K$, the canonical injection satisfies $(0 : K) < q$ if and only if $0 < q$.

NNRat.cast_lt_zero theorem

: (q : K) < 0 ↔ q < 0

Full source

@[norm_cast] lemma cast_lt_zero : (q : K) < 0 ↔ q < 0 := by norm_cast

Non-Negative Rational Cast Preserves Negative Status: $(q : K) < 0 \leftrightarrow q < 0$

Informal description

For any non-negative rational number $q$ and any linear ordered field $K$, the canonical injection satisfies $(q : K) < 0$ if and only if $q < 0$.

NNRat.not_cast_lt_zero theorem

: ¬(q : K) < 0

Full source

@[simp] lemma not_cast_lt_zero : ¬(q : K) < 0 := mod_cast not_lt_zero'

Non-Negative Rational Cast is Non-Negative: $\neg (q : K) < 0$

Informal description

For any non-negative rational number $q$ and any linear ordered field $K$, the canonical injection of $q$ into $K$ is not less than zero, i.e., $\neg (q : K) < 0$.

NNRat.cast_le_one theorem

: (p : K) ≤ 1 ↔ p ≤ 1

Full source

@[simp] lemma cast_le_one : (p : K) ≤ 1 ↔ p ≤ 1 := by norm_cast

Preservation of One Greater Than or Equal Relation under Non-Negative Rational Cast

Informal description

For any non-negative rational number $p$ and any linearly ordered field $K$, the canonical injection of $p$ into $K$ satisfies $(p : K) \leq 1$ if and only if $p \leq 1$ in $\mathbb{Q}_{\geq 0}$.

NNRat.one_le_cast theorem

: 1 ≤ (p : K) ↔ 1 ≤ p

Full source

@[simp] lemma one_le_cast : 1 ≤ (p : K) ↔ 1 ≤ p := by norm_cast

Preservation of One Less Than or Equal Relation under Non-Negative Rational Cast

Informal description

For any non-negative rational number $p$ and any linearly ordered field $K$, the canonical injection of $p$ into $K$ satisfies $1 \leq p$ in $K$ if and only if $1 \leq p$ in $\mathbb{Q}_{\geq 0}$.

NNRat.cast_lt_one theorem

: (p : K) < 1 ↔ p < 1

Full source

@[simp] lemma cast_lt_one : (p : K) < 1 ↔ p < 1 := by norm_cast

Preservation of Strict Inequality with One under Non-Negative Rational Cast

Informal description

For any non-negative rational number $p$ and any linear ordered field $K$, the canonical injection of $p$ into $K$ is less than $1$ if and only if $p$ is less than $1$ in $\mathbb{Q}_{\geq 0}$, i.e., $(p : K) < 1 \leftrightarrow p < 1$.

NNRat.one_lt_cast theorem

: 1 < (p : K) ↔ 1 < p

Full source

@[simp] lemma one_lt_cast : 1 < (p : K) ↔ 1 < p := by norm_cast

Preservation of One Less Than Relation under Non-Negative Rational Cast

Informal description

For any non-negative rational number $p$ and any linearly ordered field $K$, the canonical injection of $p$ into $K$ satisfies $1 < p$ in $K$ if and only if $1 < p$ in $\mathbb{Q}_{\geq 0}$.

NNRat.cast_le_ofNat theorem

: (p : K) ≤ ofNat(n) ↔ p ≤ OfNat.ofNat n

Full source

@[simp] lemma cast_le_ofNat : (p : K) ≤ ofNat(n) ↔ p ≤ OfNat.ofNat n := by
  simp [← cast_le (K := K)]

Nonnegative Rational Cast Preserves Order with Numerals: $(p : K) \leq n \leftrightarrow p \leq n$

Informal description

For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$, any natural number $n \geq 2$, and any linearly ordered field $K$, the canonical embedding satisfies $(p : K) \leq n$ if and only if $p \leq n$.

NNRat.ofNat_le_cast theorem

: ofNat(n) ≤ (p : K) ↔ OfNat.ofNat n ≤ p

Full source

@[simp] lemma ofNat_le_cast : ofNat(n)ofNat(n) ≤ (p : K) ↔ OfNat.ofNat n ≤ p := by
  simp [← cast_le (K := K)]

Numeral Less Than or Equal to Nonnegative Rational Cast: $n \leq (p : K) \leftrightarrow n \leq p$

Informal description

For any natural number $n$ and any nonnegative rational number $p$ in a linearly ordered field $K$, the canonical embedding satisfies $n \leq (p : K)$ if and only if $n \leq p$.

NNRat.cast_lt_ofNat theorem

: (p : K) < ofNat(n) ↔ p < OfNat.ofNat n

Full source

@[simp] lemma cast_lt_ofNat : (p : K) < ofNat(n) ↔ p < OfNat.ofNat n := by
  simp [← cast_lt (K := K)]

Nonnegative Rational Cast Preserves Strict Order with Numerals: $(p : K) < n \leftrightarrow p < n$

Informal description

For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$, any natural number $n \geq 2$, and any linearly ordered field $K$, the canonical embedding satisfies $(p : K) < n$ if and only if $p < n$.

NNRat.ofNat_lt_cast theorem

: ofNat(n) < (p : K) ↔ OfNat.ofNat n < p

Full source

@[simp] lemma ofNat_lt_cast : ofNat(n)ofNat(n) < (p : K) ↔ OfNat.ofNat n < p := by
  simp [← cast_lt (K := K)]

Numeral Strictly Less Than Nonnegative Rational Cast: $n < (p : K) \leftrightarrow n < p$

Informal description

For any natural number $n$ and any nonnegative rational number $p$ in a linearly ordered field $K$, the canonical embedding satisfies $n < (p : K)$ if and only if $n < p$.

NNRat.cast_le_natCast theorem

{m : ℚ≥0} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ≥0)

Full source

@[simp, norm_cast]
theorem cast_le_natCast {m : ℚ≥0} {n : ℕ} : (m : K) ≤ n ↔ m ≤ (n : ℚ≥0) := by
  rw [← cast_le (K := K), cast_natCast]

Nonnegative Rational Cast vs Natural Number Order: $(m : K) \leq n \leftrightarrow m \leq (n : \mathbb{Q}_{\geq 0})$

Informal description

For any nonnegative rational number $m \in \mathbb{Q}_{\geq 0}$, any natural number $n \in \mathbb{N}$, and any linearly ordered field $K$, the canonical embedding satisfies $(m : K) \leq n$ if and only if $m \leq (n : \mathbb{Q}_{\geq 0})$.

NNRat.natCast_le_cast theorem

{m : ℕ} {n : ℚ≥0} : (m : K) ≤ n ↔ (m : ℚ≥0) ≤ n

Full source

@[simp, norm_cast]
theorem natCast_le_cast {m : ℕ} {n : ℚ≥0} : (m : K) ≤ n ↔ (m : ℚ≥0) ≤ n := by
  rw [← cast_le (K := K), cast_natCast]

Natural Number to Field Cast Preserves Inequality with Nonnegative Rationals: $(m : K) \leq n \leftrightarrow (m : \mathbb{Q}_{\geq 0}) \leq n$

Informal description

For any natural number $m$, any nonnegative rational number $n \in \mathbb{Q}_{\geq 0}$, and any linearly ordered field $K$, the inequality $(m : K) \leq n$ holds if and only if $(m : \mathbb{Q}_{\geq 0}) \leq n$.

NNRat.cast_lt_natCast theorem

{m : ℚ≥0} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ≥0)

Full source

@[simp, norm_cast]
theorem cast_lt_natCast {m : ℚ≥0} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ≥0) := by
  rw [← cast_lt (K := K), cast_natCast]

Strict Order Preservation for Nonnegative Rational Cast vs Natural Numbers: $(m : K) < n \leftrightarrow m < (n : \mathbb{Q}_{\geq 0})$

Informal description

For any nonnegative rational number $m \in \mathbb{Q}_{\geq 0}$, any natural number $n \in \mathbb{N}$, and any linearly ordered field $K$, the canonical embedding satisfies $(m : K) < n$ if and only if $m < (n : \mathbb{Q}_{\geq 0})$.

NNRat.natCast_lt_cast theorem

{m : ℕ} {n : ℚ≥0} : (m : K) < n ↔ (m : ℚ≥0) < n

Full source

@[simp, norm_cast]
theorem natCast_lt_cast {m : ℕ} {n : ℚ≥0} : (m : K) < n ↔ (m : ℚ≥0) < n := by
  rw [← cast_lt (K := K), cast_natCast]

Natural Number to Field Cast Preserves Strict Inequality with Nonnegative Rationals

Informal description

For any natural number $m$ and nonnegative rational number $n$, and for any linearly ordered field $K$, the inequality $(m : K) < n$ holds if and only if $(m : \mathbb{Q}_{\geq 0}) < n$.

NNRat.cast_min theorem

(p q : ℚ≥0) : (↑(min p q) : K) = min (p : K) (q : K)

Full source

@[simp, norm_cast] lemma cast_min (p q : ℚ≥0) : (↑(min p q) : K) = min (p : K) (q : K) :=
  (@cast_mono K _).map_min

Preservation of Minimum under Canonical Map from Nonnegative Rationals to Ordered Field

Informal description

For any nonnegative rational numbers $p$ and $q$, and any linear ordered field $K$, the canonical map from $\mathbb{Q}_{\geq 0}$ to $K$ preserves the minimum operation. That is, $\min(p, q) = \min(p_K, q_K)$, where $p_K$ and $q_K$ denote the images of $p$ and $q$ in $K$ under the canonical map.

NNRat.cast_max theorem

(p q : ℚ≥0) : (↑(max p q) : K) = max (p : K) (q : K)

Full source

@[simp, norm_cast] lemma cast_max (p q : ℚ≥0) : (↑(max p q) : K) = max (p : K) (q : K) :=
  (@cast_mono K _).map_max

Preservation of Maximum under Canonical Map from Nonnegative Rationals to Ordered Field

Informal description

For any nonnegative rational numbers $p$ and $q$, and any linear ordered field $K$, the canonical map from $\mathbb{Q}_{\geq 0}$ to $K$ preserves the maximum operation. That is, $\max(p, q)$ in $\mathbb{Q}_{\geq 0}$ maps to $\max(p, q)$ in $K$.

NNRat.preimage_cast_Icc theorem

(p q : ℚ≥0) : (↑) ⁻¹' Icc (p : K) q = Icc p q

Full source

@[simp]
theorem preimage_cast_Icc (p q : ℚ≥0) : (↑) ⁻¹' Icc (p : K) q = Icc p q :=
  castOrderEmbedding.preimage_Icc ..

Preimage of Closed Interval under Nonnegative Rational Embedding Equals Original Interval

Informal description

For any nonnegative rational numbers $p, q \in \mathbb{Q}_{\geq 0}$, the preimage under the canonical embedding $\mathbb{Q}_{\geq 0} \hookrightarrow K$ of the closed interval $[p, q]$ in the linearly ordered field $K$ is equal to the closed interval $[p, q]$ in $\mathbb{Q}_{\geq 0}$. That is, $$ (\mathbb{Q}_{\geq 0} \hookrightarrow K)^{-1}\big([p, q]\big) = [p, q]. $$

NNRat.preimage_cast_Ico theorem

(p q : ℚ≥0) : (↑) ⁻¹' Ico (p : K) q = Ico p q

Full source

@[simp]
theorem preimage_cast_Ico (p q : ℚ≥0) : (↑) ⁻¹' Ico (p : K) q = Ico p q :=
  castOrderEmbedding.preimage_Ico ..

Preimage of Closed-Open Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q}_{\geq 0} \hookrightarrow K$ of the closed-open interval $[p, q)$ in the linearly ordered field $K$ is equal to the closed-open interval $[p, q)$ in $\mathbb{Q}_{\geq 0}$. That is, $$ (\uparrow)^{-1}\big([p, q)\big) = [p, q). $$

NNRat.preimage_cast_Ioc theorem

(p q : ℚ≥0) : (↑) ⁻¹' Ioc (p : K) q = Ioc p q

Full source

@[simp]
theorem preimage_cast_Ioc (p q : ℚ≥0) : (↑) ⁻¹' Ioc (p : K) q = Ioc p q :=
  castOrderEmbedding.preimage_Ioc p q

Preimage of Open-Closed Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q}_{\geq 0} \hookrightarrow K$ of the open-closed interval $(p, q]$ in the linearly ordered field $K$ is equal to the open-closed interval $(p, q]$ in $\mathbb{Q}_{\geq 0}$. That is, $$ (\uparrow)^{-1}\big((p, q]\big) = (p, q]. $$

NNRat.preimage_cast_Ioo theorem

(p q : ℚ≥0) : (↑) ⁻¹' Ioo (p : K) q = Ioo p q

Full source

@[simp]
theorem preimage_cast_Ioo (p q : ℚ≥0) : (↑) ⁻¹' Ioo (p : K) q = Ioo p q :=
  castOrderEmbedding.preimage_Ioo p q

Preimage of Open Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational numbers $p$ and $q$, the preimage under the canonical embedding of the open interval $(p, q)$ in a linearly ordered field $K$ is equal to the open interval $(p, q)$ in $\mathbb{Q}_{\geq 0}$. That is, $$ (\uparrow)^{-1}\big((p, q)\big) = (p, q). $$

NNRat.preimage_cast_Ici theorem

(p : ℚ≥0) : (↑) ⁻¹' Ici (p : K) = Ici p

Full source

@[simp]
theorem preimage_cast_Ici (p : ℚ≥0) : (↑) ⁻¹' Ici (p : K) = Ici p :=
  castOrderEmbedding.preimage_Ici p

Preimage of Closed Right-Infinite Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$, the preimage under the canonical embedding $\mathbb{Q}_{\geq 0} \hookrightarrow K$ of the closed right-infinite interval $[p, \infty)$ in the linearly ordered field $K$ is equal to the closed right-infinite interval $[p, \infty)$ in $\mathbb{Q}_{\geq 0}$, i.e., $$ (\uparrow)^{-1}\big([p, \infty)\big) = [p, \infty). $$

NNRat.preimage_cast_Iic theorem

(p : ℚ≥0) : (↑) ⁻¹' Iic (p : K) = Iic p

Full source

@[simp]
theorem preimage_cast_Iic (p : ℚ≥0) : (↑) ⁻¹' Iic (p : K) = Iic p :=
  castOrderEmbedding.preimage_Iic p

Preimage of Closed Left-Infinite Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$, the preimage under the canonical embedding $\mathbb{Q}_{\geq 0} \hookrightarrow K$ of the closed left-infinite interval $(-\infty, p]$ in the linearly ordered field $K$ is equal to the closed left-infinite interval $(-\infty, p]$ in $\mathbb{Q}_{\geq 0}$, i.e., $$ (\uparrow)^{-1}\big((-\infty, p]\big) = (-\infty, p]. $$

NNRat.preimage_cast_Ioi theorem

(p : ℚ≥0) : (↑) ⁻¹' Ioi (p : K) = Ioi p

Full source

@[simp]
theorem preimage_cast_Ioi (p : ℚ≥0) : (↑) ⁻¹' Ioi (p : K) = Ioi p :=
  castOrderEmbedding.preimage_Ioi p

Preimage of Strict Right-Infinite Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$ and any linearly ordered field $K$, the preimage under the canonical embedding of the strict right-infinite interval $(p, \infty)$ in $K$ is equal to the strict right-infinite interval $(p, \infty)$ in $\mathbb{Q}_{\geq 0}$, i.e., $$ (\uparrow)^{-1}\big((p, \infty)\big) = (p, \infty). $$

NNRat.preimage_cast_Iio theorem

(p : ℚ≥0) : (↑) ⁻¹' Iio (p : K) = Iio p

Full source

@[simp]
theorem preimage_cast_Iio (p : ℚ≥0) : (↑) ⁻¹' Iio (p : K) = Iio p :=
  castOrderEmbedding.preimage_Iio p

Preimage of Strict Left-Infinite Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational number $p \in \mathbb{Q}_{\geq 0}$, the preimage under the canonical embedding into a linearly ordered field $K$ of the strict left-infinite interval $(-\infty, p)$ in $K$ is equal to the strict left-infinite interval $(-\infty, p)$ in $\mathbb{Q}_{\geq 0}$, i.e., $(\uparrow)^{-1}((-\infty, p)) = (-\infty, p)$.

NNRat.preimage_cast_uIcc theorem

(p q : ℚ≥0) : (↑) ⁻¹' uIcc (p : K) q = uIcc p q

Full source

@[simp]
theorem preimage_cast_uIcc (p q : ℚ≥0) : (↑) ⁻¹' uIcc (p : K) q = uIcc p q :=
  (castOrderEmbedding (K := K)).preimage_uIcc p q

Preimage of Unordered Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q}_{\geq 0} \hookrightarrow K$ of the unordered closed interval $[p \sqcap q, p \sqcup q]$ in the linearly ordered field $K$ is equal to the unordered closed interval $[p \sqcap q, p \sqcup q]$ in $\mathbb{Q}_{\geq 0}$. That is, $$ (\uparrow)^{-1}\big([p \sqcap q, p \sqcup q]\big) = [p \sqcap q, p \sqcup q]. $$

NNRat.preimage_cast_uIoc theorem

(p q : ℚ≥0) : (↑) ⁻¹' uIoc (p : K) q = uIoc p q

Full source

@[simp]
theorem preimage_cast_uIoc (p q : ℚ≥0) : (↑) ⁻¹' uIoc (p : K) q = uIoc p q :=
  (castOrderEmbedding (K := K)).preimage_uIoc p q

Preimage of Generalized Open-Closed Interval under Nonnegative Rational Embedding

Informal description

For any nonnegative rational numbers $p$ and $q$, the preimage under the canonical embedding $\mathbb{Q}_{\geq 0} \hookrightarrow K$ of the generalized open-closed interval $(p, q]$ in the linearly ordered field $K$ is equal to the generalized open-closed interval $(p, q]$ in $\mathbb{Q}_{\geq 0}$. That is, $$ (\uparrow)^{-1}\big((\min(p, q), \max(p, q)]\big) = (\min(p, q), \max(p, q)]. $$

Mathlib.Meta.Positivity.evalRatCast definition

: PositivityExt

Full source

/-- Extension for Rat.cast. -/
@[positivity Rat.cast _]
def evalRatCast : PositivityExt where eval {u α} _zα _pα e := do
  let ~q(@Rat.cast _ (_) ($a : ℚ)) := e | throwError "not Rat.cast"
  match ← core q(inferInstance) q(inferInstance) a with
  | .positive pa =>
    let _oα ← synthInstanceQ q(Field $α)
    let _oα ← synthInstanceQ q(LinearOrder $α)
    let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
    assumeInstancesCommute
    return .positive q((Rat.cast_pos (K := $α)).mpr $pa)
  | .nonnegative pa =>
    let _oα ← synthInstanceQ q(Field $α)
    let _oα ← synthInstanceQ q(LinearOrder $α)
    let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
    assumeInstancesCommute
    return .nonnegative q((Rat.cast_nonneg (K := $α)).mpr $pa)
  | .nonzero pa =>
    let _oα ← synthInstanceQ q(DivisionRing $α)
    let _cα ← synthInstanceQ q(CharZero $α)
    assumeInstancesCommute
    return .nonzero q((Rat.cast_ne_zero (α := $α)).mpr $pa)
  | .none => pure .none

Positivity evaluation for rational number casts in linear ordered fields

Informal description

The function evaluates the positivity of a rational number cast into a linear ordered field. Given a rational number $a$ and a linear ordered field $\alpha$, it determines whether the cast of $a$ into $\alpha$ is positive, nonnegative, nonzero, or none of these. Specifically: 1. If $a$ is positive in $\mathbb{Q}$, then its cast in $\alpha$ is positive. 2. If $a$ is nonnegative in $\mathbb{Q}$, then its cast in $\alpha$ is nonnegative. 3. If $a$ is nonzero in $\mathbb{Q}$ and $\alpha$ is a division ring of characteristic zero, then its cast in $\alpha$ is nonzero. 4. Otherwise, no conclusion is drawn about the positivity of the cast.

Mathlib.Meta.Positivity.evalNNRatCast definition

: PositivityExt

Full source

/-- Extension for NNRat.cast. -/
@[positivity NNRat.cast _]
def evalNNRatCast : PositivityExt where eval {u α} _zα _pα e := do
  let ~q(@NNRat.cast _ (_) ($a : ℚ≥0)) := e | throwError "not NNRat.cast"
  match ← core q(inferInstance) q(inferInstance) a with
  | .positive pa =>
    let _oα ← synthInstanceQ q(Semifield $α)
    let _oα ← synthInstanceQ q(LinearOrder $α)
    let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
    assumeInstancesCommute
    return .positive q((NNRat.cast_pos (K := $α)).mpr $pa)
  | _ =>
    let _oα ← synthInstanceQ q(Semifield $α)
    let _oα ← synthInstanceQ q(LinearOrder $α)
    let _oα ← synthInstanceQ q(IsStrictOrderedRing $α)
    assumeInstancesCommute
    return .nonnegative q(NNRat.cast_nonneg _)

Positivity of non-negative rational number casts in ordered semifields

Informal description

The positivity extension for non-negative rational number casts evaluates whether the cast of a non-negative rational number `a : ℚ≥0` into a linear ordered semifield `α` is positive or non-negative. Specifically: - If `a` is positive, then its cast in `α` is also positive. - Otherwise, the cast is non-negative. This assumes `α` is a semifield with a linear order and strict ordered ring structure.