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 {K : Type u_5} [LinearOrderedField K] {r : ℚ} (hr : 0 < r) :
0 < ↑r
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 {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℚ} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp]
theorem Rat.cast_lt {K : Type u_5} [LinearOrderedField K] {m : ℚ} {n : ℚ} :
↑m < ↑n ↔ m < n
source
@[simp]
theorem Rat.cast_nonneg {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
0 ≤ ↑n ↔ 0 ≤ n
source
@[simp]
theorem Rat.cast_nonpos {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
↑n ≤ 0 ↔ n ≤ 0
source
@[simp]
theorem Rat.cast_pos {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
0 < ↑n ↔ 0 < n
source
@[simp]
theorem Rat.cast_lt_zero {K : Type u_5} [LinearOrderedField K] {n : ℚ} :
↑n < 0 ↔ n < 0
source
@[simp]
theorem Rat.cast_min {K : Type u_5} [LinearOrderedField K] {a : ℚ} {b : ℚ} :
↑(min a b) = min ↑a ↑b
source
@[simp]
theorem Rat.cast_max {K : Type u_5} [LinearOrderedField K] {a : ℚ} {b : ℚ} :
↑(max a b) = max ↑a ↑b
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] (a : ℚ) (b : ℚ) :
Rat.cast ⁻¹' Set.Icc ↑a ↑b = Set.Icc a b
source
@[simp]
theorem Rat.preimage_cast_Ico {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
Rat.cast ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
source
@[simp]
theorem Rat.preimage_cast_Ioc {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
Rat.cast ⁻¹' Set.Ioc ↑a ↑b = Set.Ioc a b
source
@[simp]
theorem Rat.preimage_cast_Ioo {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
Rat.cast ⁻¹' Set.Ioo ↑a ↑b = Set.Ioo a b
source
@[simp]
theorem Rat.preimage_cast_Ici {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
Rat.cast ⁻¹' Set.Ici ↑a = Set.Ici a
source
@[simp]
theorem Rat.preimage_cast_Iic {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
Rat.cast ⁻¹' Set.Iic ↑a = Set.Iic a
source
@[simp]
theorem Rat.preimage_cast_Ioi {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
Rat.cast ⁻¹' Set.Ioi ↑a = Set.Ioi a
source
@[simp]
theorem Rat.preimage_cast_Iio {K : Type u_5} [LinearOrderedField K] (a : ℚ) :
Rat.cast ⁻¹' Set.Iio ↑a = Set.Iio a
source
@[simp]
theorem Rat.preimage_cast_uIcc {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
Rat.cast ⁻¹' Set.uIcc ↑a ↑b = Set.uIcc a b
source
@[simp]
theorem Rat.preimage_cast_uIoc {K : Type u_5} [LinearOrderedField K] (a : ℚ) (b : ℚ) :
Rat.cast ⁻¹' Ι ↑a ↑b = Ι a b
source
def Mathlib.Meta.Positivity.evalRatCast :
Mathlib.Meta.Positivity.PositivityExt

Extension for Rat.cast.