data.rat.order

# Order for Rational Numbers #

## Summary #

We define the order on ℚ, prove that ℚ is a discrete, linearly ordered field, and define functions such as abs and sqrt that depend on this order.

## Notations #

• /. is infix notation for rat.mk.

## Tags #

rat, rationals, field, ℚ, numerator, denominator, num, denom, order, ordering, sqrt, abs

@[protected]
def rat.nonneg (r : ) :
Prop

A rational number is called nonnegative if its numerator is nonnegative.

Equations
Instances for rat.nonneg
@[simp]
theorem rat.mk_nonneg (a : ) {b : } (h : 0 < b) :
(rat.mk a b).nonneg 0 a
@[protected]
theorem rat.nonneg_add {a b : } :
a.nonnegb.nonneg(a + b).nonneg
@[protected]
theorem rat.nonneg_mul {a b : } :
a.nonnegb.nonneg(a * b).nonneg
@[protected]
theorem rat.nonneg_antisymm {a : } :
a.nonneg(-a).nonnega = 0
@[protected]
theorem rat.nonneg_total (a : ) :
@[protected, instance]
def rat.decidable_nonneg (a : ) :
Equations
@[protected, irreducible]
def rat.le (a b : ) :
Prop

Relation a ≤ b on ℚ defined as a ≤ b ↔ rat.nonneg (b - a). Use a ≤ b instead of rat.le a b.

Equations
@[protected, instance]
def rat.has_le  :
Equations
@[protected, instance]
Equations
@[protected]
theorem rat.le_def {a b c d : } (b0 : 0 < b) (d0 : 0 < d) :
b d a * d c * b
@[protected]
theorem rat.le_refl (a : ) :
a a
@[protected]
theorem rat.le_total (a b : ) :
a b b a
@[protected]
theorem rat.le_antisymm {a b : } (hab : a b) (hba : b a) :
a = b
@[protected]
theorem rat.le_trans {a b c : } (hab : a b) (hbc : b c) :
a c
@[protected, instance]
Equations
@[protected, instance]
def rat.has_lt  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def rat.lattice  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def rat.has_inf  :
Equations
@[protected, instance]
def rat.has_sup  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem rat.le_def' {p q : } :
p q p.num * (q.denom) q.num * (p.denom)
@[protected]
theorem rat.lt_def {p q : } :
p < q p.num * (q.denom) < q.num * (p.denom)
theorem rat.nonneg_iff_zero_le {a : } :
a.nonneg 0 a
theorem rat.num_nonneg_iff_zero_le {a : } :
0 a.num 0 a
@[protected]
c + a c + b a b
@[protected]
theorem rat.mul_nonneg {a b : } (ha : 0 a) (hb : 0 b) :
0 a * b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem rat.num_pos_iff_pos {a : } :
0 < a.num 0 < a
theorem rat.div_lt_div_iff_mul_lt_mul {a b c d : } (b_pos : 0 < b) (d_pos : 0 < d) :
a / b < c / d a * d < c * b
theorem rat.lt_one_iff_num_lt_denom {q : } :
q < 1 q.num < (q.denom)
theorem rat.abs_def (q : ) :