mathlib docs: data.rat.order

a.decidable_nonneg = a.cases_on (λ (a_num : ℤ) (a_denom : ℕ) (a_pos : 0 < a_denom) (a_cop : a_num.nat_abs.coprime a_denom), _.mpr (0.decidable_le a_num))

source

def rat.le :

ℚ → ℚ → Prop

Equations

a.le b = (b - a).nonneg

source

@[instance]

def rat.has_le :

has_le ℚ

Equations

rat.has_le = {le := rat.le}

source

@[instance]

def rat.decidable_le :

decidable_rel has_le.le

Equations

rat.decidable_le a b = show decidable (b - a).nonneg, from (b - a).decidable_nonneg

source

theorem rat.le_def {a b c d : ℤ} :

0 < b → 0 < d → (rat.mk a b ≤ rat.mk c d ↔ a * d ≤ c * b)

source

theorem rat.le_refl (a : ℚ) :

a ≤ a

source

theorem rat.le_total (a b : ℚ) :

a ≤ b ∨ b ≤ a

source

theorem rat.le_antisymm {a b : ℚ} :

a ≤ b → b ≤ a → a = b

source

theorem rat.le_trans {a b c : ℚ} :

a ≤ b → b ≤ c → a ≤ c

source

@[instance]

def rat.decidable_linear_order :

decidable_linear_order ℚ

Equations

rat.decidable_linear_order = {le := rat.le, lt := linear_order.lt._default rat.le, le_refl := rat.le_refl, le_trans := rat.le_trans, lt_iff_le_not_le := rat.decidable_linear_order._proof_1, le_antisymm := rat.le_antisymm, le_total := rat.le_total, decidable_le := λ (a b : ℚ), (b - a).decidable_nonneg, decidable_eq := λ (a b : ℚ), rat.decidable_eq a b, decidable_lt := decidable_lt_of_decidable_le (λ (a b : ℚ), (b - a).decidable_nonneg)}

source

@[instance]

def rat.has_lt :

has_lt ℚ

Equations

rat.has_lt = preorder.to_has_lt ℚ

source

@[instance]

def rat.distrib_lattice :

distrib_lattice ℚ

Equations

rat.distrib_lattice = distrib_lattice_of_decidable_linear_order

source

@[instance]

def rat.lattice :

lattice ℚ

Equations

rat.lattice = lattice_of_decidable_linear_order

source

@[instance]

def rat.semilattice_inf :

semilattice_inf ℚ

Equations

rat.semilattice_inf = lattice.to_semilattice_inf ℚ

source

@[instance]

def rat.semilattice_sup :

semilattice_sup ℚ

Equations

rat.semilattice_sup = lattice.to_semilattice_sup ℚ

source

@[instance]

def rat.has_inf :

has_inf ℚ

Equations

rat.has_inf = semilattice_inf.to_has_inf ℚ

source

@[instance]

def rat.has_sup :

has_sup ℚ

Equations

rat.has_sup = semilattice_sup.to_has_sup ℚ

source

@[instance]

def rat.linear_order :

linear_order ℚ

Equations

rat.linear_order = decidable_linear_order.to_linear_order ℚ

source

@[instance]

def rat.partial_order :

partial_order ℚ

Equations

rat.partial_order = semilattice_inf.to_partial_order ℚ

source

@[instance]

def rat.preorder :

preorder ℚ

Equations

rat.preorder = directed_order.to_preorder

source

theorem rat.le_def' {p q : ℚ} :

p ≤ q ↔ p.num * ↑(q.denom) ≤ q.num * ↑(p.denom)

source

theorem rat.lt_def {p q : ℚ} :

p < q ↔ p.num * ↑(q.denom) < q.num * ↑(p.denom)

source

theorem rat.nonneg_iff_zero_le {a : ℚ} :

a.nonneg ↔ 0 ≤ a

source

theorem rat.num_nonneg_iff_zero_le {a : ℚ} :

0 ≤ a.num ↔ 0 ≤ a

source

theorem rat.add_le_add_left {a b c : ℚ} :

c + a ≤ c + b ↔ a ≤ b

source

theorem rat.mul_nonneg {a b : ℚ} :

0 ≤ a → 0 ≤ b → 0 ≤ a * b

source

@[instance]

def rat.discrete_linear_ordered_field :

discrete_linear_ordered_field ℚ

Equations

rat.discrete_linear_ordered_field = {add := field.add rat.field, add_assoc := _, zero := field.zero rat.field, zero_add := _, add_zero := _, neg := field.neg rat.field, add_left_neg := _, add_comm := _, mul := field.mul rat.field, mul_assoc := _, one := field.one rat.field, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := decidable_linear_order.le rat.decidable_linear_order, lt := decidable_linear_order.lt rat.decidable_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := rat.discrete_linear_ordered_field._proof_1, exists_pair_ne := _, mul_pos := rat.discrete_linear_ordered_field._proof_2, le_total := _, zero_lt_one := rat.discrete_linear_ordered_field._proof_3, mul_comm := _, inv := field.inv rat.field, mul_inv_cancel := _, inv_zero := _, decidable_le := decidable_linear_order.decidable_le rat.decidable_linear_order, decidable_eq := decidable_linear_order.decidable_eq rat.decidable_linear_order, decidable_lt := decidable_linear_order.decidable_lt rat.decidable_linear_order}

source

@[instance]

def rat.linear_ordered_field :

linear_ordered_field ℚ

Equations

rat.linear_ordered_field = discrete_linear_ordered_field.to_linear_ordered_field ℚ

source

@[instance]

def rat.decidable_linear_ordered_comm_ring :

decidable_linear_ordered_comm_ring ℚ

Equations

rat.decidable_linear_ordered_comm_ring = discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring ℚ

source

@[instance]

def rat.linear_ordered_comm_ring :

linear_ordered_comm_ring ℚ

Equations

rat.linear_ordered_comm_ring = linear_ordered_field.to_linear_ordered_comm_ring ℚ

source

@[instance]

def rat.linear_ordered_ring :

linear_ordered_ring ℚ

Equations

rat.linear_ordered_ring = linear_ordered_comm_ring.to_linear_ordered_ring ℚ

source

@[instance]

def rat.ordered_ring :

ordered_ring ℚ

Equations

rat.ordered_ring = linear_ordered_ring.to_ordered_ring ℚ

source

@[instance]

def rat.decidable_linear_ordered_semiring :

decidable_linear_ordered_semiring ℚ

Equations

rat.decidable_linear_ordered_semiring = decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_semiring

source

@[instance]

def rat.linear_ordered_semiring :

linear_ordered_semiring ℚ

Equations

rat.linear_ordered_semiring = linear_ordered_ring.to_linear_ordered_semiring

source

@[instance]

def rat.ordered_semiring :

ordered_semiring ℚ

Equations

rat.ordered_semiring = ordered_ring.to_ordered_semiring

source

@[instance]

def rat.decidable_linear_ordered_add_comm_group :

decidable_linear_ordered_add_comm_group ℚ

Equations

rat.decidable_linear_ordered_add_comm_group = decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_add_comm_group ℚ

source

@[instance]

def rat.ordered_add_comm_group :

ordered_add_comm_group ℚ

Equations

rat.ordered_add_comm_group = ordered_ring.to_ordered_add_comm_group ℚ

source

@[instance]

def rat.ordered_cancel_add_comm_monoid :

ordered_cancel_add_comm_monoid ℚ

Equations

rat.ordered_cancel_add_comm_monoid = ordered_semiring.to_ordered_cancel_add_comm_monoid ℚ

source

@[instance]

def rat.ordered_add_comm_monoid :

ordered_add_comm_monoid ℚ

Equations

rat.ordered_add_comm_monoid = ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid

source

theorem rat.num_pos_iff_pos {a : ℚ} :

0 < a.num ↔ 0 < a

source

theorem rat.div_lt_div_iff_mul_lt_mul {a b c d : ℤ} :

0 < b → 0 < d → (↑a / ↑b < ↑c / ↑d ↔ a * d < c * b)

source

theorem rat.lt_one_iff_num_lt_denom {q : ℚ} :

q < 1 ↔ q.num < ↑(q.denom)

source

theorem rat.abs_def (q : ℚ) :

abs q = rat.mk ↑(q.num.nat_abs) ↑(q.denom)

mathlib documentation

data.rat.order

Order for Rational Numbers

Summary

Notations

Tags

General documentation

Additional documentation

Library

mathlib documentation

data.​rat.​order

Order for Rational Numbers

Summary

Notations

Tags

General documentation

Additional documentation

Library

data.rat.order