Documentation

Mathlib.Data.Rat.Cast.Order

Casts of rational numbers into linear ordered fields. #

theorem Rat.cast_pos_of_pos {q : } {K : Type u_5} [LinearOrderedField K] (hq : 0 < q) :
0 < q
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 {p : } {q : } {K : Type u_5} [LinearOrderedField K] :
    p q p q
    @[simp]
    theorem Rat.cast_lt {p : } {q : } {K : Type u_5} [LinearOrderedField K] :
    p < q p < q
    @[simp]
    theorem Rat.cast_nonneg {q : } {K : Type u_5} [LinearOrderedField K] :
    0 q 0 q
    @[simp]
    theorem Rat.cast_nonpos {q : } {K : Type u_5} [LinearOrderedField K] :
    q 0 q 0
    @[simp]
    theorem Rat.cast_pos {q : } {K : Type u_5} [LinearOrderedField K] :
    0 < q 0 < q
    @[simp]
    theorem Rat.cast_lt_zero {q : } {K : Type u_5} [LinearOrderedField K] :
    q < 0 q < 0
    @[simp]
    theorem Rat.cast_le_natCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m n m n
    @[simp]
    theorem Rat.natCast_le_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m n m n
    @[simp]
    theorem Rat.cast_le_intCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m n m n
    @[simp]
    theorem Rat.intCast_le_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m n m n
    @[simp]
    theorem Rat.cast_lt_natCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m < n m < n
    @[simp]
    theorem Rat.natCast_lt_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m < n m < n
    @[simp]
    theorem Rat.cast_lt_intCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m < n m < n
    @[simp]
    theorem Rat.intCast_lt_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
    m < n m < n
    @[simp]
    theorem Rat.cast_min {K : Type u_5} [LinearOrderedField K] (p : ) (q : ) :
    (min p q) = min p q
    @[simp]
    theorem Rat.cast_max {K : Type u_5} [LinearOrderedField K] (p : ) (q : ) :
    (max p q) = max p q
    @[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] (p : ) (q : ) :
    Rat.cast ⁻¹' Set.Icc p q = Set.Icc p q
    @[simp]
    theorem Rat.preimage_cast_Ico {K : Type u_5} [LinearOrderedField K] (p : ) (q : ) :
    Rat.cast ⁻¹' Set.Ico p q = Set.Ico p q
    @[simp]
    theorem Rat.preimage_cast_Ioc {K : Type u_5} [LinearOrderedField K] (p : ) (q : ) :
    Rat.cast ⁻¹' Set.Ioc p q = Set.Ioc p q
    @[simp]
    theorem Rat.preimage_cast_Ioo {K : Type u_5} [LinearOrderedField K] (p : ) (q : ) :
    Rat.cast ⁻¹' Set.Ioo p q = Set.Ioo p q
    @[simp]
    theorem Rat.preimage_cast_Ici {K : Type u_5} [LinearOrderedField K] (q : ) :
    Rat.cast ⁻¹' Set.Ici q = Set.Ici q
    @[simp]
    theorem Rat.preimage_cast_Iic {K : Type u_5} [LinearOrderedField K] (q : ) :
    Rat.cast ⁻¹' Set.Iic q = Set.Iic q
    @[simp]
    theorem Rat.preimage_cast_Ioi {K : Type u_5} [LinearOrderedField K] (q : ) :
    Rat.cast ⁻¹' Set.Ioi q = Set.Ioi q
    @[simp]
    theorem Rat.preimage_cast_Iio {K : Type u_5} [LinearOrderedField K] (q : ) :
    Rat.cast ⁻¹' Set.Iio q = Set.Iio q
    @[simp]
    theorem Rat.preimage_cast_uIcc {K : Type u_5} [LinearOrderedField K] (p : ) (q : ) :
    Rat.cast ⁻¹' Set.uIcc p q = Set.uIcc p q
    @[simp]
    theorem Rat.preimage_cast_uIoc {K : Type u_5} [LinearOrderedField K] (p : ) (q : ) :
    Rat.cast ⁻¹' Ι p q = Ι p q
    theorem NNRat.cast_mono {K : Type u_5} [LinearOrderedSemifield K] :
    Monotone NNRat.cast
    @[simp]
    theorem NNRat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedSemifield K] :
    ∀ (a : ℚ≥0), NNRat.castOrderEmbedding a = a

    Coercion from as an order embedding.

    Equations
    Instances For
      @[simp]
      theorem NNRat.cast_le {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {q : ℚ≥0} :
      p q p q
      @[simp]
      theorem NNRat.cast_lt {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {q : ℚ≥0} :
      p < q p < q
      @[simp]
      theorem NNRat.cast_nonpos {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      q 0 q 0
      @[simp]
      theorem NNRat.cast_pos {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      0 < q 0 < q
      theorem NNRat.cast_lt_zero {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      q < 0 q < 0
      @[simp]
      theorem NNRat.not_cast_lt_zero {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      ¬q < 0
      @[simp]
      theorem NNRat.cast_le_one {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      p 1 p 1
      @[simp]
      theorem NNRat.one_le_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      1 p 1 p
      @[simp]
      theorem NNRat.cast_lt_one {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      p < 1 p < 1
      @[simp]
      theorem NNRat.one_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      1 < p 1 < p
      @[simp]
      theorem NNRat.cast_le_ofNat {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : } [n.AtLeastTwo] :
      @[simp]
      theorem NNRat.ofNat_le_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : } [n.AtLeastTwo] :
      @[simp]
      theorem NNRat.cast_lt_ofNat {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : } [n.AtLeastTwo] :
      @[simp]
      theorem NNRat.ofNat_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : } [n.AtLeastTwo] :
      @[simp]
      theorem NNRat.cast_le_natCast {K : Type u_5} [LinearOrderedSemifield K] {m : ℚ≥0} {n : } :
      m n m n
      @[simp]
      theorem NNRat.natCast_le_cast {K : Type u_5} [LinearOrderedSemifield K] {m : } {n : ℚ≥0} :
      m n m n
      @[simp]
      theorem NNRat.cast_lt_natCast {K : Type u_5} [LinearOrderedSemifield K] {m : ℚ≥0} {n : } :
      m < n m < n
      @[simp]
      theorem NNRat.natCast_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {m : } {n : ℚ≥0} :
      m < n m < n
      @[simp]
      theorem NNRat.cast_min {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      (min p q) = min p q
      @[simp]
      theorem NNRat.cast_max {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      (max p q) = max p q
      @[simp]
      theorem NNRat.preimage_cast_Icc {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Icc p q = Set.Icc p q
      @[simp]
      theorem NNRat.preimage_cast_Ico {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ico p q = Set.Ico p q
      @[simp]
      theorem NNRat.preimage_cast_Ioc {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ioc p q = Set.Ioc p q
      @[simp]
      theorem NNRat.preimage_cast_Ioo {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ioo p q = Set.Ioo p q
      @[simp]
      theorem NNRat.preimage_cast_Ici {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ici p = Set.Ici p
      @[simp]
      theorem NNRat.preimage_cast_Iic {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Iic p = Set.Iic p
      @[simp]
      theorem NNRat.preimage_cast_Ioi {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ioi p = Set.Ioi p
      @[simp]
      theorem NNRat.preimage_cast_Iio {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Iio p = Set.Iio p
      @[simp]
      theorem NNRat.preimage_cast_uIcc {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.uIcc p q = Set.uIcc p q
      @[simp]
      theorem NNRat.preimage_cast_uIoc {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
      NNRat.cast ⁻¹' Ι p q = Ι p q