Documentation

Mathlib.Data.Rat.Cast.Order

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_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
source
@[simp]
theorem Rat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedField K] (a✝ : ℚ) :
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
source
@[simp]
theorem NNRat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedSemifield K] (a✝ : ℚ≥0) :
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 :
PositivityExt

Extension for Rat.cast.

source
def Mathlib.Meta.Positivity.evalNNRatCast :
PositivityExt

Extension for NNRat.cast.