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
@[simp]
theorem Rat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedField K] :
∀ (a : ℚ), Rat.castOrderEmbedding a = ↑a
source
def Rat.castOrderEmbedding {K : Type u_5} [LinearOrderedField K] :
ℚ ↪o K

Coercion from ℚ as an order embedding.

Equations
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
@[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_min {K : Type u_5} [LinearOrderedField K] (p : ℚ) (q : ℚ) :
↑(min p q) = min ↑p ↑q
source
@[simp]
theorem Rat.cast_max {K : Type u_5} [LinearOrderedField K] (p : ℚ) (q : ℚ) :
↑(max p q) = max ↑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
@[simp]
theorem NNRat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedSemifield K] :
∀ (a : ℚ≥0), NNRat.castOrderEmbedding a = ↑a
source
def NNRat.castOrderEmbedding {K : Type u_5} [LinearOrderedSemifield K] :
ℚ≥0 ↪o K

Coercion from ℚ as an order embedding.

Equations
source
@[simp]
theorem NNRat.cast_le {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {q : ℚ≥0} :
↑p ≤ ↑q ↔ p ≤ q
source
@[simp]
theorem NNRat.cast_lt {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} {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_min {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
↑(min p q) = min ↑p ↑q
source
@[simp]
theorem NNRat.cast_max {K : Type u_5} [LinearOrderedSemifield K] (p : ℚ≥0) (q : ℚ≥0) :
↑(max p q) = max ↑p ↑q
source
@[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
source
@[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
source
@[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
source
@[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
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 : ℚ≥0) (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 : ℚ≥0) (q : ℚ≥0) :
NNRat.cast ⁻¹' Ι ↑p ↑q = Ι p q
source
def Mathlib.Meta.Positivity.evalRatCast :
Mathlib.Meta.Positivity.PositivityExt

Extension for Rat.cast.

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

Extension for NNRat.cast.