# Casts of rational numbers into linear ordered fields. #

@[simp]
theorem Rat.castHom_rat :
theorem Rat.cast_pos_of_pos {q : } {K : Type u_5} (hq : 0 < q) :
0 < q
theorem Rat.cast_strictMono {K : Type u_5} :
StrictMono Rat.cast
theorem Rat.cast_mono {K : Type u_5} :
Monotone Rat.cast
@[simp]
theorem Rat.castOrderEmbedding_apply {K : Type u_5} :
∀ (a : ), Rat.castOrderEmbedding a = a

Coercion from ℚ as an order embedding.

Equations
Instances For
@[simp]
theorem Rat.cast_le {p : } {q : } {K : Type u_5} :
p q p q
@[simp]
theorem Rat.cast_lt {p : } {q : } {K : Type u_5} :
p < q p < q
@[simp]
theorem Rat.cast_nonneg {q : } {K : Type u_5} :
0 q 0 q
@[simp]
theorem Rat.cast_nonpos {q : } {K : Type u_5} :
q 0 q 0
@[simp]
theorem Rat.cast_pos {q : } {K : Type u_5} :
0 < q 0 < q
@[simp]
theorem Rat.cast_lt_zero {q : } {K : Type u_5} :
q < 0 q < 0
@[simp]
theorem Rat.cast_min {K : Type u_5} (p : ) (q : ) :
(min p q) = min p q
@[simp]
theorem Rat.cast_max {K : Type u_5} (p : ) (q : ) :
(max p q) = max p q
@[simp]
theorem Rat.cast_abs {K : Type u_5} (q : ) :
|q| = |q|
@[simp]
theorem Rat.preimage_cast_Icc {K : Type u_5} (p : ) (q : ) :
Rat.cast ⁻¹' Set.Icc p q = Set.Icc p q
@[simp]
theorem Rat.preimage_cast_Ico {K : Type u_5} (p : ) (q : ) :
Rat.cast ⁻¹' Set.Ico p q = Set.Ico p q
@[simp]
theorem Rat.preimage_cast_Ioc {K : Type u_5} (p : ) (q : ) :
Rat.cast ⁻¹' Set.Ioc p q = Set.Ioc p q
@[simp]
theorem Rat.preimage_cast_Ioo {K : Type u_5} (p : ) (q : ) :
Rat.cast ⁻¹' Set.Ioo p q = Set.Ioo p q
@[simp]
theorem Rat.preimage_cast_Ici {K : Type u_5} (q : ) :
Rat.cast ⁻¹' Set.Ici q =
@[simp]
theorem Rat.preimage_cast_Iic {K : Type u_5} (q : ) :
Rat.cast ⁻¹' Set.Iic q =
@[simp]
theorem Rat.preimage_cast_Ioi {K : Type u_5} (q : ) :
Rat.cast ⁻¹' Set.Ioi q =
@[simp]
theorem Rat.preimage_cast_Iio {K : Type u_5} (q : ) :
Rat.cast ⁻¹' Set.Iio q =
@[simp]
theorem Rat.preimage_cast_uIcc {K : Type u_5} (p : ) (q : ) :
Rat.cast ⁻¹' Set.uIcc p q = Set.uIcc p q
@[simp]
theorem Rat.preimage_cast_uIoc {K : Type u_5} (p : ) (q : ) :
Rat.cast ⁻¹' Ι p q = Ι p q
theorem NNRat.cast_strictMono {K : Type u_5} :
StrictMono NNRat.cast
theorem NNRat.cast_mono {K : Type u_5} :
Monotone NNRat.cast
@[simp]
theorem NNRat.castOrderEmbedding_apply {K : Type u_5} :
∀ (a : ℚ≥0), NNRat.castOrderEmbedding a = a

Coercion from ℚ as an order embedding.

Equations
Instances For
@[simp]
theorem NNRat.cast_le {K : Type u_5} {p : ℚ≥0} {q : ℚ≥0} :
p q p q
@[simp]
theorem NNRat.cast_lt {K : Type u_5} {p : ℚ≥0} {q : ℚ≥0} :
p < q p < q
@[simp]
theorem NNRat.cast_nonpos {K : Type u_5} {q : ℚ≥0} :
q 0 q 0
@[simp]
theorem NNRat.cast_pos {K : Type u_5} {q : ℚ≥0} :
0 < q 0 < q
theorem NNRat.cast_lt_zero {K : Type u_5} {q : ℚ≥0} :
q < 0 q < 0
@[simp]
theorem NNRat.not_cast_lt_zero {K : Type u_5} {q : ℚ≥0} :
¬q < 0
@[simp]
theorem NNRat.cast_min {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
(min p q) = min p q
@[simp]
theorem NNRat.cast_max {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
(max p q) = max p q
@[simp]
theorem NNRat.preimage_cast_Icc {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
NNRat.cast ⁻¹' Set.Icc p q = Set.Icc p q
@[simp]
theorem NNRat.preimage_cast_Ico {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
NNRat.cast ⁻¹' Set.Ico p q = Set.Ico p q
@[simp]
theorem NNRat.preimage_cast_Ioc {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
NNRat.cast ⁻¹' Set.Ioc p q = Set.Ioc p q
@[simp]
theorem NNRat.preimage_cast_Ioo {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
NNRat.cast ⁻¹' Set.Ioo p q = Set.Ioo p q
@[simp]
theorem NNRat.preimage_cast_Ici {K : Type u_5} (p : ℚ≥0) :
NNRat.cast ⁻¹' Set.Ici p =
@[simp]
theorem NNRat.preimage_cast_Iic {K : Type u_5} (p : ℚ≥0) :
NNRat.cast ⁻¹' Set.Iic p =
@[simp]
theorem NNRat.preimage_cast_Ioi {K : Type u_5} (p : ℚ≥0) :
NNRat.cast ⁻¹' Set.Ioi p =
@[simp]
theorem NNRat.preimage_cast_Iio {K : Type u_5} (p : ℚ≥0) :
NNRat.cast ⁻¹' Set.Iio p =
@[simp]
theorem NNRat.preimage_cast_uIcc {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
NNRat.cast ⁻¹' Set.uIcc p q = Set.uIcc p q
@[simp]
theorem NNRat.preimage_cast_uIoc {K : Type u_5} (p : ℚ≥0) (q : ℚ≥0) :
NNRat.cast ⁻¹' Ι p q = Ι p q

Extension for Rat.cast.

Instances For

Extension for NNRat.cast.

Instances For