Documentation

Mathlib.Data.Rat.Cast.Order

Casts of rational numbers into linear ordered fields. #

theorem Rat.cast_pos_of_pos {K : Type u_5} [LinearOrderedField K] {r : } (hr : 0 < r) :
0 < r
theorem Rat.cast_mono {K : Type u_5} [LinearOrderedField K] :
Monotone Rat.cast
@[simp]
theorem Rat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedField K] :
∀ (a : ), Rat.castOrderEmbedding a = a

Coercion from as an order embedding.

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