Documentation

Mathlib.Data.Rat.Cast.Order

Casts of rational numbers into linear ordered fields. #

source
@[simp]
theorem Rat.castHom_rat :
Rat.castHom ℚ = RingHom.id ℚ
source
theorem Rat.cast_pos_of_pos {K : Type u_5} [LinearOrderedField K] {r : ℚ} (hr : 0 < r) :
0 < ↑r
source
theorem Rat.cast_strictMono {K : Type u_5} [LinearOrderedField K] :
StrictMono Rat.cast
source
theorem Rat.cast_mono {K : Type u_5} [LinearOrderedField K] :
Monotone Rat.cast
source
@[simp]
theorem Rat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedField K] :
∀ (a : ℚ), ↑Rat.castOrderEmbedding a = ↑a
source
def Rat.castOrderEmbedding {K : Type u_5} [LinearOrderedField K] :
ℚ ↪o K

Coercion from ℚ as an order embedding.

Equations
Instances For
    source
    @[simp]
    theorem Rat.cast_le {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℚ} :
    ↑m ≤ ↑n ↔ m ≤ n
    source
    @[simp]
    theorem Rat.cast_lt {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℚ} :
    ↑m < ↑n ↔ m < n
    source
    @[simp]
    theorem Rat.cast_nonneg {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
    0 ≤ ↑n ↔ 0 ≤ n
    source
    @[simp]
    theorem Rat.cast_nonpos {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
    ↑n ≤ 0 ↔ n ≤ 0
    source
    @[simp]
    theorem Rat.cast_pos {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
    0 < ↑n ↔ 0 < n
    source
    @[simp]
    theorem Rat.cast_lt_zero {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
    ↑n < 0 ↔ n < 0
    source
    @[simp]
    theorem Rat.cast_min {K : Type u_5} [LinearOrderedField K] {a : ℚ} {b : ℚ} :
    ↑(min a b) = min ↑a ↑b
    source
    @[simp]
    theorem Rat.cast_max {K : Type u_5} [LinearOrderedField K] {a : ℚ} {b : ℚ} :
    ↑(max a b) = max ↑a ↑b
    source
    @[simp]
    theorem Rat.cast_abs {K : Type u_5} [LinearOrderedField K] {q : ℚ} :
    ↑|q| = |↑q|
    source
    @[simp]
    theorem Rat.preimage_cast_Icc {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
    Rat.cast ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
    source
    @[simp]
    theorem Rat.preimage_cast_Ico {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
    Rat.cast ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
    source
    @[simp]
    theorem Rat.preimage_cast_Ioc {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
    Rat.cast ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
    source
    @[simp]
    theorem Rat.preimage_cast_Ioo {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
    Rat.cast ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
    source
    @[simp]
    theorem Rat.preimage_cast_Ici {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
    Rat.cast ⁻¹' Set.Ici ↑a = Set.Ici a
    source
    @[simp]
    theorem Rat.preimage_cast_Iic {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
    Rat.cast ⁻¹' Set.Iic ↑a = Set.Iic a
    source
    @[simp]
    theorem Rat.preimage_cast_Ioi {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
    Rat.cast ⁻¹' Set.Ioi ↑a = Set.Ioi a
    source
    @[simp]
    theorem Rat.preimage_cast_Iio {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
    Rat.cast ⁻¹' Set.Iio ↑a = Set.Iio a