HepLean 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 {q : ℚ} {K : Type u_5} [LinearOrderedField K] (hq : 0 < q) :
0 < ↑q
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
def Rat.castOrderEmbedding {K : Type u_5} [LinearOrderedField K] :
ℚ ↪o K

Coercion from ℚ as an order embedding.

Equations
Instances For
    source
    @[simp]
    theorem Rat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedField K] (a✝ : ℚ) :
    Rat.castOrderEmbedding a✝ = ↑a✝
    source
    @[simp]
    theorem Rat.cast_le {p q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    ↑p ≤ ↑q ↔ p ≤ q
    source
    @[simp]
    theorem Rat.cast_lt {p q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    ↑p < ↑q ↔ p < q
    source
    theorem GCongr.ratCast_le_ratCast {p q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    p ≤ q → ↑p ≤ ↑q

    Alias of the reverse direction of Rat.cast_le.

    source
    theorem GCongr.ratCast_lt_ratCast {p q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    p < q → ↑p < ↑q

    Alias of the reverse direction of Rat.cast_lt.

    source
    @[simp]
    theorem Rat.cast_nonneg {q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    0 ≤ ↑q ↔ 0 ≤ q
    source
    @[simp]
    theorem Rat.cast_nonpos {q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    ↑q ≤ 0 ↔ q ≤ 0
    source
    @[simp]
    theorem Rat.cast_pos {q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    0 < ↑q ↔ 0 < q
    source
    @[simp]
    theorem Rat.cast_lt_zero {q : ℚ} {K : Type u_5} [LinearOrderedField K] :
    ↑q < 0 ↔ q < 0
    source
    @[simp]
    theorem Rat.cast_le_natCast {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℕ} :
    ↑m ≤ ↑n ↔ m ≤ ↑n
    source
    @[simp]
    theorem Rat.natCast_le_cast {K : Type u_5} [LinearOrderedField K] {m : ℕ} {n : ℚ} :
    ↑m ≤ ↑n ↔ ↑m ≤ n
    source
    @[simp]
    theorem Rat.cast_le_intCast {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℤ} :
    ↑m ≤ ↑n ↔ m ≤ ↑n
    source
    @[simp]
    theorem Rat.intCast_le_cast {K : Type u_5} [LinearOrderedField K] {m : ℤ} {n : ℚ} :
    ↑m ≤ ↑n ↔ ↑m ≤ n
    source
    @[simp]
    theorem Rat.cast_lt_natCast {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℕ} :
    ↑m < ↑n ↔ m < ↑n
    source
    @[simp]
    theorem Rat.natCast_lt_cast {K : Type u_5} [LinearOrderedField K] {m : ℕ} {n : ℚ} :
    ↑m < ↑n ↔ ↑m < n
    source
    @[simp]
    theorem Rat.cast_lt_intCast {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℤ} :
    ↑m < ↑n ↔ m < ↑n
    source
    @[simp]
    theorem Rat.intCast_lt_cast {K : Type u_5} [LinearOrderedField K] {m : ℤ} {n : ℚ} :
    ↑m < ↑n ↔ ↑m < n
    source
    @[simp]
    theorem Rat.cast_min {K : Type u_5} [LinearOrderedField K] (p q : ℚ) :
    ↑(p ⊓ q) = ↑p ⊓ ↑q
    source
    @[simp]
    theorem Rat.cast_max {K : Type u_5} [LinearOrderedField K] (p q : ℚ) :
    ↑(p ⊔ q) = ↑p ⊔ ↑q
    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] (p q : ℚ) :
    Rat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q
    source
    @[simp]
    theorem Rat.preimage_cast_Ico {K : Type u_5} [LinearOrderedField K] (p q : ℚ) :
    Rat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q
    source
    @[simp]
    theorem Rat.preimage_cast_Ioc {K : Type u_5} [LinearOrderedField K] (p q : ℚ) :
    Rat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q
    source
    @[simp]
    theorem Rat.preimage_cast_Ioo {K : Type u_5} [LinearOrderedField K] (p q : ℚ) :
    Rat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q
    source
    @[simp]
    theorem Rat.preimage_cast_Ici {K : Type u_5} [LinearOrderedField K] (q : ℚ) :
    Rat.cast ⁻¹' Set.Ici ↑q = Set.Ici q
    source
    @[simp]
    theorem Rat.preimage_cast_Iic {K : Type u_5} [LinearOrderedField K] (q : ℚ) :
    Rat.cast ⁻¹' Set.Iic ↑q = Set.Iic q
    source
    @[simp]
    theorem Rat.preimage_cast_Ioi {K : Type u_5} [LinearOrderedField K] (q : ℚ) :
    Rat.cast ⁻¹' Set.Ioi ↑q = Set.Ioi q
    source
    @[simp]
    theorem Rat.preimage_cast_Iio {K : Type u_5} [LinearOrderedField K] (q : ℚ) :
    Rat.cast ⁻¹' Set.Iio ↑q = Set.Iio q
    source
    @[simp]
    theorem Rat.preimage_cast_uIcc {K : Type u_5} [LinearOrderedField K] (p q : ℚ) :
    Rat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
    source
    @[simp]
    theorem Rat.preimage_cast_uIoc {K : Type u_5} [LinearOrderedField K] (p q : ℚ) :
    Rat.cast ⁻¹' Ι ↑p ↑q = Ι p q
    source
    theorem NNRat.cast_strictMono {K : Type u_5} [LinearOrderedSemifield K] :
    StrictMono NNRat.cast
    source
    theorem NNRat.cast_mono {K : Type u_5} [LinearOrderedSemifield K] :
    Monotone NNRat.cast
    source
    def NNRat.castOrderEmbedding {K : Type u_5} [LinearOrderedSemifield K] :
    ℚ≥0 ↪o K

    Coercion from ℚ as an order embedding.

    Equations
    Instances For
      source
      @[simp]
      theorem NNRat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedSemifield K] (a✝ : ℚ≥0) :
      NNRat.castOrderEmbedding a✝ = ↑a✝
      source
      @[simp]
      theorem NNRat.cast_le {K : Type u_5} [LinearOrderedSemifield K] {p q : ℚ≥0} :
      ↑p ≤ ↑q ↔ p ≤ q
      source
      @[simp]
      theorem NNRat.cast_lt {K : Type u_5} [LinearOrderedSemifield K] {p q : ℚ≥0} :
      ↑p < ↑q ↔ p < q
      source
      @[simp]
      theorem NNRat.cast_nonpos {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      ↑q ≤ 0 ↔ q ≤ 0
      source
      @[simp]
      theorem NNRat.cast_pos {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      0 < ↑q ↔ 0 < q
      source
      theorem NNRat.cast_lt_zero {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      ↑q < 0 ↔ q < 0
      source
      @[simp]
      theorem NNRat.not_cast_lt_zero {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
      ¬↑q < 0
      source
      @[simp]
      theorem NNRat.cast_le_one {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      ↑p ≤ 1 ↔ p ≤ 1
      source
      @[simp]
      theorem NNRat.one_le_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      1 ≤ ↑p ↔ 1 ≤ p
      source
      @[simp]
      theorem NNRat.cast_lt_one {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      ↑p < 1 ↔ p < 1
      source
      @[simp]
      theorem NNRat.one_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
      1 < ↑p ↔ 1 < p
      source
      @[simp]
      theorem NNRat.cast_le_ofNat {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :
      ↑p ≤ OfNat.ofNat n ↔ p ≤ OfNat.ofNat n
      source
      @[simp]
      theorem NNRat.ofNat_le_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :
      OfNat.ofNat n ≤ ↑p ↔ OfNat.ofNat n ≤ p
      source
      @[simp]
      theorem NNRat.cast_lt_ofNat {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :
      ↑p < OfNat.ofNat n ↔ p < OfNat.ofNat n
      source
      @[simp]
      theorem NNRat.ofNat_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :
      OfNat.ofNat n < ↑p ↔ OfNat.ofNat n < p
      source
      @[simp]
      theorem NNRat.cast_le_natCast {K : Type u_5} [LinearOrderedSemifield K] {m : ℚ≥0} {n : ℕ} :
      ↑m ≤ ↑n ↔ m ≤ ↑n
      source
      @[simp]
      theorem NNRat.natCast_le_cast {K : Type u_5} [LinearOrderedSemifield K] {m : ℕ} {n : ℚ≥0} :
      ↑m ≤ ↑n ↔ ↑m ≤ n
      source
      @[simp]
      theorem NNRat.cast_lt_natCast {K : Type u_5} [LinearOrderedSemifield K] {m : ℚ≥0} {n : ℕ} :
      ↑m < ↑n ↔ m < ↑n
      source
      @[simp]
      theorem NNRat.natCast_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {m : ℕ} {n : ℚ≥0} :
      ↑m < ↑n ↔ ↑m < n
      source
      @[simp]
      theorem NNRat.cast_min {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      ↑(p ⊓ q) = ↑p ⊓ ↑q
      source
      @[simp]
      theorem NNRat.cast_max {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      ↑(p ⊔ q) = ↑p ⊔ ↑q
      source
      @[simp]
      theorem NNRat.preimage_cast_Icc {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q
      source
      @[simp]
      theorem NNRat.preimage_cast_Ico {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q
      source
      @[simp]
      theorem NNRat.preimage_cast_Ioc {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q
      source
      @[simp]
      theorem NNRat.preimage_cast_Ioo {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q
      source
      @[simp]
      theorem NNRat.preimage_cast_Ici {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ici ↑p = Set.Ici p
      source
      @[simp]
      theorem NNRat.preimage_cast_Iic {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Iic ↑p = Set.Iic p
      source
      @[simp]
      theorem NNRat.preimage_cast_Ioi {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Ioi ↑p = Set.Ioi p
      source
      @[simp]
      theorem NNRat.preimage_cast_Iio {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) :
      NNRat.cast ⁻¹' Set.Iio ↑p = Set.Iio p
      source
      @[simp]
      theorem NNRat.preimage_cast_uIcc {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      NNRat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q
      source
      @[simp]
      theorem NNRat.preimage_cast_uIoc {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
      NNRat.cast ⁻¹' Ι ↑p ↑q = Ι p q
      source
      def Mathlib.Meta.Positivity.evalRatCast :
      Mathlib.Meta.Positivity.PositivityExt

      Extension for Rat.cast.

      Instances For
        source
        def Mathlib.Meta.Positivity.evalNNRatCast :
        Mathlib.Meta.Positivity.PositivityExt

        Extension for NNRat.cast.

        Instances For