Casts of rational numbers into linear ordered fields. #

source

@[simp]

theorem Rat.castHom_rat :

castHom ℚ = RingHom.id ℚ

source

theorem Rat.cast_pos_of_pos {q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (hq : 0 < q) :

0 < ↑q

source

theorem Rat.cast_strictMono {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

StrictMono Rat.cast

source

theorem Rat.cast_mono {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

Monotone Rat.cast

source

def Rat.castOrderEmbedding {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

ℚ ↪o K

Coercion from ℚ as an order embedding.

Equations

Rat.castOrderEmbedding = OrderEmbedding.ofStrictMono Rat.cast ⋯

Instances For

source

@[simp]

theorem Rat.castOrderEmbedding_apply {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (a✝ : ℚ) :

castOrderEmbedding a✝ = ↑a✝

source

@[simp]

theorem Rat.cast_le {p q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

↑p ≤ ↑q ↔ p ≤ q

source

@[simp]

theorem Rat.cast_lt {p q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

↑p < ↑q ↔ p < q

source

@[simp]

theorem Rat.cast_nonneg {q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

0 ≤ ↑q ↔ 0 ≤ q

source

@[simp]

theorem Rat.cast_nonpos {q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

↑q ≤ 0 ↔ q ≤ 0

source

@[simp]

theorem Rat.cast_pos {q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

0 < ↑q ↔ 0 < q

source

@[simp]

theorem Rat.cast_lt_zero {q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

↑q < 0 ↔ q < 0

source

@[simp]

theorem Rat.cast_le_natCast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℕ} :

↑m ≤ ↑n ↔ m ≤ ↑n

source

@[simp]

theorem Rat.natCast_le_cast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ} :

↑m ≤ ↑n ↔ ↑m ≤ n

source

@[simp]

theorem Rat.cast_le_intCast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℤ} :

↑m ≤ ↑n ↔ m ≤ ↑n

source

@[simp]

theorem Rat.intCast_le_cast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℤ} {n : ℚ} :

↑m ≤ ↑n ↔ ↑m ≤ n

source

@[simp]

theorem Rat.cast_lt_natCast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℕ} :

↑m < ↑n ↔ m < ↑n

source

@[simp]

theorem Rat.natCast_lt_cast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ} :

↑m < ↑n ↔ ↑m < n

source

@[simp]

theorem Rat.cast_lt_intCast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℤ} :

↑m < ↑n ↔ m < ↑n

source

@[simp]

theorem Rat.intCast_lt_cast {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℤ} {n : ℚ} :

↑m < ↑n ↔ ↑m < n

source

@[simp]

theorem Rat.cast_min {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

↑(min p q) = min ↑p ↑q

source

@[simp]

theorem Rat.cast_max {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

↑(max p q) = max ↑p ↑q

source

@[simp]

theorem Rat.cast_abs {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) :

↑|q| = |↑q|

source

@[simp]

theorem Rat.preimage_cast_Icc {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

Rat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q

source

@[simp]

theorem Rat.preimage_cast_Ico {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

Rat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q

source

@[simp]

theorem Rat.preimage_cast_Ioc {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

Rat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q

source

@[simp]

theorem Rat.preimage_cast_Ioo {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

Rat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q

source

@[simp]

theorem Rat.preimage_cast_Ici {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) :

Rat.cast ⁻¹' Set.Ici ↑q = Set.Ici q

source

@[simp]

theorem Rat.preimage_cast_Iic {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) :

Rat.cast ⁻¹' Set.Iic ↑q = Set.Iic q

source

@[simp]

theorem Rat.preimage_cast_Ioi {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) :

Rat.cast ⁻¹' Set.Ioi ↑q = Set.Ioi q

source

@[simp]

theorem Rat.preimage_cast_Iio {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (q : ℚ) :

Rat.cast ⁻¹' Set.Iio ↑q = Set.Iio q

source

@[simp]

theorem Rat.preimage_cast_uIcc {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

Rat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q

source

@[simp]

theorem Rat.preimage_cast_uIoc {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ) :

Rat.cast ⁻¹' Set.uIoc ↑p ↑q = Set.uIoc p q

source

theorem NNRat.cast_strictMono {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] :

StrictMono NNRat.cast

source

theorem NNRat.cast_mono {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] :

Monotone NNRat.cast

source

def NNRat.castOrderEmbedding {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] :

ℚ≥0 ↪o K

Coercion from ℚ as an order embedding.

Equations

NNRat.castOrderEmbedding = OrderEmbedding.ofStrictMono NNRat.cast ⋯

Instances For

source

@[simp]

theorem NNRat.castOrderEmbedding_apply {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (a✝ : ℚ≥0) :

castOrderEmbedding a✝ = ↑a✝

source

@[simp]

theorem NNRat.cast_le {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p q : ℚ≥0} :

↑p ≤ ↑q ↔ p ≤ q

source

@[simp]

theorem NNRat.cast_lt {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p q : ℚ≥0} :

↑p < ↑q ↔ p < q

source

@[simp]

theorem NNRat.cast_nonpos {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :

↑q ≤ 0 ↔ q ≤ 0

source

@[simp]

theorem NNRat.cast_pos {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :

0 < ↑q ↔ 0 < q

source

theorem NNRat.cast_lt_zero {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :

↑q < 0 ↔ q < 0

source

@[simp]

theorem NNRat.not_cast_lt_zero {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0} :

¬↑q < 0

source

@[simp]

theorem NNRat.cast_le_one {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :

↑p ≤ 1 ↔ p ≤ 1

source

@[simp]

theorem NNRat.one_le_cast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :

1 ≤ ↑p ↔ 1 ≤ p

source

@[simp]

theorem NNRat.cast_lt_one {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :

↑p < 1 ↔ p < 1

source

@[simp]

theorem NNRat.one_lt_cast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} :

1 < ↑p ↔ 1 < p

source

@[simp]

theorem NNRat.cast_le_ofNat {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :

↑p ≤ OfNat.ofNat n ↔ p ≤ OfNat.ofNat n

source

@[simp]

theorem NNRat.ofNat_le_cast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :

OfNat.ofNat n ≤ ↑p ↔ OfNat.ofNat n ≤ p

source

@[simp]

theorem NNRat.cast_lt_ofNat {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :

↑p < OfNat.ofNat n ↔ p < OfNat.ofNat n

source

@[simp]

theorem NNRat.ofNat_lt_cast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ} [n.AtLeastTwo] :

OfNat.ofNat n < ↑p ↔ OfNat.ofNat n < p

source

@[simp]

theorem NNRat.cast_le_natCast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ≥0} {n : ℕ} :

↑m ≤ ↑n ↔ m ≤ ↑n

source

@[simp]

theorem NNRat.natCast_le_cast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ≥0} :

↑m ≤ ↑n ↔ ↑m ≤ n

source

@[simp]

theorem NNRat.cast_lt_natCast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℚ≥0} {n : ℕ} :

↑m < ↑n ↔ m < ↑n

source

@[simp]

theorem NNRat.natCast_lt_cast {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ≥0} :

↑m < ↑n ↔ ↑m < n

source

@[simp]

theorem NNRat.cast_min {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

↑(min p q) = min ↑p ↑q

source

@[simp]

theorem NNRat.cast_max {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

↑(max p q) = max ↑p ↑q

source

@[simp]

theorem NNRat.preimage_cast_Icc {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

NNRat.cast ⁻¹' Set.Icc ↑p ↑q = Set.Icc p q

source

@[simp]

theorem NNRat.preimage_cast_Ico {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

NNRat.cast ⁻¹' Set.Ico ↑p ↑q = Set.Ico p q

source

@[simp]

theorem NNRat.preimage_cast_Ioc {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

NNRat.cast ⁻¹' Set.Ioc ↑p ↑q = Set.Ioc p q

source

@[simp]

theorem NNRat.preimage_cast_Ioo {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

NNRat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q

source

@[simp]

theorem NNRat.preimage_cast_Ici {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0) :

NNRat.cast ⁻¹' Set.Ici ↑p = Set.Ici p

source

@[simp]

theorem NNRat.preimage_cast_Iic {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0) :

NNRat.cast ⁻¹' Set.Iic ↑p = Set.Iic p

source

@[simp]

theorem NNRat.preimage_cast_Ioi {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0) :

NNRat.cast ⁻¹' Set.Ioi ↑p = Set.Ioi p

source

@[simp]

theorem NNRat.preimage_cast_Iio {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p : ℚ≥0) :

NNRat.cast ⁻¹' Set.Iio ↑p = Set.Iio p

source

@[simp]

theorem NNRat.preimage_cast_uIcc {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

NNRat.cast ⁻¹' Set.uIcc ↑p ↑q = Set.uIcc p q

source

@[simp]

theorem NNRat.preimage_cast_uIoc {K : Type u_2} [Semifield K] [LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ≥0) :

NNRat.cast ⁻¹' Set.uIoc ↑p ↑q = Set.uIoc p q

source

def Mathlib.Meta.Positivity.evalRatCast :

PositivityExt

Extension for Rat.cast.

Instances For

source

def Mathlib.Meta.Positivity.evalNNRatCast :

PositivityExt

Extension for NNRat.cast.

Instances For

Documentation

Mathlib.Data.Rat.Cast.Order

Casts of rational numbers into linear ordered fields. #