Documentation

Mathlib.Data.Rat.Cast.Order

Casts of rational numbers into linear ordered fields. #

theorem Rat.cast_pos_of_pos {q : } {K : Type u_5} [LinearOrderedField K] (hq : 0 < q) :
0 < q

Coercion from as an order embedding.

Equations
@[simp]
theorem Rat.castOrderEmbedding_apply {K : Type u_5} [LinearOrderedField K] (a✝ : ) :
castOrderEmbedding a✝ = a✝
@[simp]
theorem Rat.cast_le {p q : } {K : Type u_5} [LinearOrderedField K] :
p q p q
@[simp]
theorem Rat.cast_lt {p q : } {K : Type u_5} [LinearOrderedField K] :
p < q p < q
theorem GCongr.ratCast_le_ratCast {p q : } {K : Type u_5} [LinearOrderedField K] :
p qp q

Alias of the reverse direction of Rat.cast_le.

theorem GCongr.ratCast_lt_ratCast {p q : } {K : Type u_5} [LinearOrderedField K] :
p < qp < q

Alias of the reverse direction of Rat.cast_lt.

@[simp]
theorem Rat.cast_nonneg {q : } {K : Type u_5} [LinearOrderedField K] :
0 q 0 q
@[simp]
theorem Rat.cast_nonpos {q : } {K : Type u_5} [LinearOrderedField K] :
q 0 q 0
@[simp]
theorem Rat.cast_pos {q : } {K : Type u_5} [LinearOrderedField K] :
0 < q 0 < q
@[simp]
theorem Rat.cast_lt_zero {q : } {K : Type u_5} [LinearOrderedField K] :
q < 0 q < 0
@[simp]
theorem Rat.cast_le_natCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m n m n
@[simp]
theorem Rat.natCast_le_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m n m n
@[simp]
theorem Rat.cast_le_intCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m n m n
@[simp]
theorem Rat.intCast_le_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m n m n
@[simp]
theorem Rat.cast_lt_natCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m < n m < n
@[simp]
theorem Rat.natCast_lt_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m < n m < n
@[simp]
theorem Rat.cast_lt_intCast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m < n m < n
@[simp]
theorem Rat.intCast_lt_cast {K : Type u_5} [LinearOrderedField K] {m : } {n : } :
m < n m < n
@[simp]
theorem Rat.cast_min {K : Type u_5} [LinearOrderedField K] (p q : ) :
↑(p q) = p q
@[simp]
theorem Rat.cast_max {K : Type u_5} [LinearOrderedField K] (p q : ) :
↑(p q) = p q
@[simp]
theorem Rat.cast_abs {K : Type u_5} [LinearOrderedField K] (q : ) :
|q| = |q|
@[simp]
theorem Rat.preimage_cast_Icc {K : Type u_5} [LinearOrderedField K] (p q : ) :
@[simp]
theorem Rat.preimage_cast_Ico {K : Type u_5} [LinearOrderedField K] (p q : ) :
@[simp]
theorem Rat.preimage_cast_Ioc {K : Type u_5} [LinearOrderedField K] (p q : ) :
@[simp]
theorem Rat.preimage_cast_Ioo {K : Type u_5} [LinearOrderedField K] (p q : ) :
@[simp]
theorem Rat.preimage_cast_uIcc {K : Type u_5} [LinearOrderedField K] (p q : ) :
@[simp]
theorem Rat.preimage_cast_uIoc {K : Type u_5} [LinearOrderedField K] (p q : ) :
Rat.cast ⁻¹' Ι p q = Ι p q
@[simp]
theorem NNRat.cast_le {K : Type u_5} [LinearOrderedSemifield K] {p q : ℚ≥0} :
p q p q
@[simp]
theorem NNRat.cast_lt {K : Type u_5} [LinearOrderedSemifield K] {p q : ℚ≥0} :
p < q p < q
@[simp]
theorem NNRat.cast_nonpos {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
q 0 q 0
@[simp]
theorem NNRat.cast_pos {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
0 < q 0 < q
theorem NNRat.cast_lt_zero {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
q < 0 q < 0
@[simp]
theorem NNRat.not_cast_lt_zero {K : Type u_5} [LinearOrderedSemifield K] {q : ℚ≥0} :
¬q < 0
@[simp]
theorem NNRat.cast_le_one {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
p 1 p 1
@[simp]
theorem NNRat.one_le_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
1 p 1 p
@[simp]
theorem NNRat.cast_lt_one {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
p < 1 p < 1
@[simp]
theorem NNRat.one_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {p : ℚ≥0} :
1 < p 1 < p
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem NNRat.cast_le_natCast {K : Type u_5} [LinearOrderedSemifield K] {m : ℚ≥0} {n : } :
m n m n
@[simp]
theorem NNRat.natCast_le_cast {K : Type u_5} [LinearOrderedSemifield K] {m : } {n : ℚ≥0} :
m n m n
@[simp]
theorem NNRat.cast_lt_natCast {K : Type u_5} [LinearOrderedSemifield K] {m : ℚ≥0} {n : } :
m < n m < n
@[simp]
theorem NNRat.natCast_lt_cast {K : Type u_5} [LinearOrderedSemifield K] {m : } {n : ℚ≥0} :
m < n m < n
@[simp]
theorem NNRat.cast_min {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
↑(p q) = p q
@[simp]
theorem NNRat.cast_max {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
↑(p q) = p q
@[simp]
theorem NNRat.preimage_cast_uIoc {K : Type u_5} [LinearOrderedSemifield K] (p q : ℚ≥0) :
NNRat.cast ⁻¹' Ι p q = Ι p q