mathlib3 documentation

data.rat.nnrat

Nonnegative rationals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the nonnegative rationals as a subtype of rat and provides its algebraic order structure.

We also define an instance can_lift ℚ ℚ≥0. This instance can be used by the lift tactic to replace x : ℚ and hx : 0 ≤ x in the proof context with x : ℚ≥0 while replacing all occurences of x with ↑x. This tactic also works for a function f : α → ℚ with a hypothesis hf : ∀ x, 0 ≤ f x.

Notation #

ℚ≥0 is notation for nnrat in locale nnrat.

@[protected, instance]

def nnrat.canonically_linear_ordered_semifield :

canonically_linear_ordered_semifield nnrat

@[protected, instance]

def nnrat.linear_ordered_comm_group_with_zero :

linear_ordered_comm_group_with_zero nnrat

@[protected, instance]

def nnrat.archimedean :

archimedean nnrat

@[protected, instance]

def nnrat.has_sub :

@[protected, instance]

def nnrat.has_ordered_sub :

has_ordered_sub nnrat

def nnrat :

Nonnegative rational numbers.

Equations

nnrat = {q // 0 ≤ q}

Instances for nnrat

@[protected, instance]

def nnrat.inhabited :

inhabited nnrat

@[protected, instance]

def nnrat.densely_ordered :

densely_ordered nnrat

@[protected, instance]

def nnrat.canonically_ordered_comm_semiring :

canonically_ordered_comm_semiring nnrat

@[protected, instance]

def nnrat.rat.has_coe :

has_coe nnrat ℚ

Equations

nnrat.rat.has_coe = {coe := subtype.val (λ (q : ℚ), 0 ≤ q)}

@[simp]

theorem nnrat.val_eq_coe (q : nnrat) :

@[protected, instance]

def nnrat.can_lift :

can_lift ℚ nnrat coe (λ (q : ℚ), 0 ≤ q)

Equations

nnrat.can_lift = {prf := nnrat.can_lift._proof_1}

@[ext]

theorem nnrat.ext {p q : nnrat} :

↑p = ↑q → p = q

@[protected]

theorem nnrat.coe_injective :

function.injective coe

@[simp, norm_cast]

theorem nnrat.coe_inj {p q : nnrat} :

↑p = ↑q ↔ p = q

theorem nnrat.ext_iff {p q : nnrat} :

p = q ↔ ↑p = ↑q

theorem nnrat.ne_iff {x y : nnrat} :

↑x ≠ ↑y ↔ x ≠ y

@[norm_cast]

theorem nnrat.coe_mk (q : ℚ) (hq : 0 ≤ q) :

↑⟨q, hq⟩ = q

def rat.to_nnrat (q : ℚ) :

Reinterpret a rational number q as a non-negative rational number. Returns 0 if q ≤ 0.

Equations

q.to_nnrat = ⟨linear_order.max q 0, _⟩

theorem rat.coe_to_nnrat (q : ℚ) (hq : 0 ≤ q) :

↑(q.to_nnrat) = q

theorem rat.le_coe_to_nnrat (q : ℚ) :

q ≤ ↑(q.to_nnrat)

@[simp]

theorem nnrat.coe_nonneg (q : nnrat) :

@[simp, norm_cast]

theorem nnrat.coe_zero :

↑0 = 0

@[simp, norm_cast]

theorem nnrat.coe_one :

↑1 = 1

@[simp, norm_cast]

theorem nnrat.coe_add (p q : nnrat) :

↑(p + q) = ↑p + ↑q

@[simp, norm_cast]

theorem nnrat.coe_mul (p q : nnrat) :

↑(p * q) = ↑p * ↑q

@[simp, norm_cast]

theorem nnrat.coe_inv (q : nnrat) :

↑q⁻¹ = (↑q)⁻¹

@[simp, norm_cast]

theorem nnrat.coe_div (p q : nnrat) :

↑(p / q) = ↑p / ↑q

@[simp, norm_cast]

theorem nnrat.coe_bit0 (q : nnrat) :

↑(bit0 q) = bit0 ↑q

@[simp, norm_cast]

theorem nnrat.coe_bit1 (q : nnrat) :

↑(bit1 q) = bit1 ↑q

@[simp, norm_cast]

theorem nnrat.coe_sub {p q : nnrat} (h : q ≤ p) :

↑(p - q) = ↑p - ↑q

@[simp]

theorem nnrat.coe_eq_zero {q : nnrat} :

↑q = 0 ↔ q = 0

theorem nnrat.coe_ne_zero {q : nnrat} :

↑q ≠ 0 ↔ q ≠ 0

@[simp, norm_cast]

theorem nnrat.coe_le_coe {p q : nnrat} :

↑p ≤ ↑q ↔ p ≤ q

@[simp, norm_cast]

theorem nnrat.coe_lt_coe {p q : nnrat} :

↑p < ↑q ↔ p < q

@[simp, norm_cast]

theorem nnrat.coe_pos {q : nnrat} :

0 < ↑q ↔ 0 < q

theorem nnrat.coe_mono :

theorem nnrat.to_nnrat_mono :

monotone rat.to_nnrat

@[simp]

theorem nnrat.to_nnrat_coe (q : nnrat) :

↑q.to_nnrat = q

@[simp]

theorem nnrat.to_nnrat_coe_nat (n : ℕ) :

↑n.to_nnrat = ↑n

@[protected]

def nnrat.gi :

galois_insertion rat.to_nnrat coe

to_nnrat and coe : ℚ≥0 → ℚ form a Galois insertion.

Equations

nnrat.gi = galois_insertion.monotone_intro nnrat.coe_mono nnrat.to_nnrat_mono rat.le_coe_to_nnrat nnrat.to_nnrat_coe

def nnrat.coe_hom :

nnrat →+* ℚ

Coercion ℚ≥0 → ℚ as a ring_hom.

Equations

nnrat.coe_hom = {to_fun := coe coe_to_lift, map_one' := nnrat.coe_one, map_mul' := nnrat.coe_mul, map_zero' := nnrat.coe_zero, map_add' := nnrat.coe_add}

@[simp, norm_cast]

theorem nnrat.coe_nat_cast (n : ℕ) :

@[simp]

theorem nnrat.mk_coe_nat (n : ℕ) :

⟨↑n, _⟩ = ↑n

@[protected, instance]

def nnrat.rat.algebra :

algebra nnrat ℚ

The rational numbers are an algebra over the non-negative rationals.

Equations

nnrat.rat.algebra = nnrat.coe_hom.to_algebra

@[protected, instance]

def nnrat.mul_action {α : Type u_1} [mul_action ℚ α] :

mul_action nnrat α

A mul_action over ℚ restricts to a mul_action over ℚ≥0.

Equations

nnrat.mul_action = mul_action.comp_hom α nnrat.coe_hom.to_monoid_hom

@[protected, instance]

def nnrat.distrib_mul_action {α : Type u_1} [add_comm_monoid α] [distrib_mul_action ℚ α] :

distrib_mul_action nnrat α

A distrib_mul_action over ℚ restricts to a distrib_mul_action over ℚ≥0.

Equations

nnrat.distrib_mul_action = distrib_mul_action.comp_hom α nnrat.coe_hom.to_monoid_hom

@[protected, instance]

def nnrat.module {α : Type u_1} [add_comm_monoid α] [module ℚ α] :

module nnrat α

A module over ℚ restricts to a module over ℚ≥0.

Equations

nnrat.module = module.comp_hom α nnrat.coe_hom

@[simp]

theorem nnrat.coe_coe_hom :

⇑nnrat.coe_hom = coe

@[simp, norm_cast]

theorem nnrat.coe_indicator {α : Type u_1} (s : set α) (f : α → nnrat) (a : α) :

↑(s.indicator f a) = s.indicator (λ (x : α), ↑(f x)) a

@[simp, norm_cast]

theorem nnrat.coe_pow (q : nnrat) (n : ℕ) :

↑(q ^ n) = ↑q ^ n

@[norm_cast]

theorem nnrat.coe_list_sum (l : list nnrat) :

↑(l.sum) = (list.map coe l).sum

@[norm_cast]

theorem nnrat.coe_list_prod (l : list nnrat) :

↑(l.prod) = (list.map coe l).prod

@[norm_cast]

theorem nnrat.coe_multiset_sum (s : multiset nnrat) :

↑(s.sum) = (multiset.map coe s).sum

@[norm_cast]

theorem nnrat.coe_multiset_prod (s : multiset nnrat) :

↑(s.prod) = (multiset.map coe s).prod

@[norm_cast]

theorem nnrat.coe_sum {α : Type u_1} {s : finset α} {f : α → nnrat} :

↑(s.sum (λ (a : α), f a)) = s.sum (λ (a : α), ↑(f a))

theorem nnrat.to_nnrat_sum_of_nonneg {α : Type u_1} {s : finset α} {f : α → ℚ} (hf : ∀ (a : α), a ∈ s → 0 ≤ f a) :

(s.sum (λ (a : α), f a)).to_nnrat = s.sum (λ (a : α), (f a).to_nnrat)

@[norm_cast]

theorem nnrat.coe_prod {α : Type u_1} {s : finset α} {f : α → nnrat} :

↑(s.prod (λ (a : α), f a)) = s.prod (λ (a : α), ↑(f a))

theorem nnrat.to_nnrat_prod_of_nonneg {α : Type u_1} {s : finset α} {f : α → ℚ} (hf : ∀ (a : α), a ∈ s → 0 ≤ f a) :

(s.prod (λ (a : α), f a)).to_nnrat = s.prod (λ (a : α), (f a).to_nnrat)

@[norm_cast]

theorem nnrat.nsmul_coe (q : nnrat) (n : ℕ) :

↑(n • q) = n • ↑q

theorem nnrat.bdd_above_coe {s : set nnrat} :

bdd_above (coe '' s) ↔ bdd_above s

theorem nnrat.bdd_below_coe (s : set nnrat) :

bdd_below (coe '' s)

@[simp, norm_cast]

theorem nnrat.coe_max (x y : nnrat) :

↑(linear_order.max x y) = linear_order.max ↑x ↑y

@[simp, norm_cast]

theorem nnrat.coe_min (x y : nnrat) :

↑(linear_order.min x y) = linear_order.min ↑x ↑y

theorem nnrat.sub_def (p q : nnrat) :

p - q = (↑p - ↑q).to_nnrat

@[simp]

theorem nnrat.abs_coe (q : nnrat) :

@[simp]

theorem rat.to_nnrat_zero :

@[simp]

theorem rat.to_nnrat_one :

@[simp]

theorem rat.to_nnrat_pos {q : ℚ} :

0 < q.to_nnrat ↔ 0 < q

@[simp]

theorem rat.to_nnrat_eq_zero {q : ℚ} :

q.to_nnrat = 0 ↔ q ≤ 0

theorem rat.to_nnrat_of_nonpos {q : ℚ} :

q ≤ 0 → q.to_nnrat = 0

Alias of the reverse direction of rat.to_nnrat_eq_zero.

@[simp]

theorem rat.to_nnrat_le_to_nnrat_iff {p q : ℚ} (hp : 0 ≤ p) :

q.to_nnrat ≤ p.to_nnrat ↔ q ≤ p

@[simp]

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

q.to_nnrat < p.to_nnrat ↔ q < p ∧ 0 < p

theorem rat.to_nnrat_lt_to_nnrat_iff {p q : ℚ} (h : 0 < p) :

q.to_nnrat < p.to_nnrat ↔ q < p

theorem rat.to_nnrat_lt_to_nnrat_iff_of_nonneg {p q : ℚ} (hq : 0 ≤ q) :

q.to_nnrat < p.to_nnrat ↔ q < p

@[simp]

theorem rat.to_nnrat_add {p q : ℚ} (hq : 0 ≤ q) (hp : 0 ≤ p) :

(q + p).to_nnrat = q.to_nnrat + p.to_nnrat

theorem rat.to_nnrat_add_le {p q : ℚ} :

(q + p).to_nnrat ≤ q.to_nnrat + p.to_nnrat

theorem rat.to_nnrat_le_iff_le_coe {q : ℚ} {p : nnrat} :

q.to_nnrat ≤ p ↔ q ≤ ↑p

theorem rat.le_to_nnrat_iff_coe_le {p : ℚ} {q : nnrat} (hp : 0 ≤ p) :

q ≤ p.to_nnrat ↔ ↑q ≤ p

theorem rat.le_to_nnrat_iff_coe_le' {p : ℚ} {q : nnrat} (hq : 0 < q) :

q ≤ p.to_nnrat ↔ ↑q ≤ p

theorem rat.to_nnrat_lt_iff_lt_coe {q : ℚ} {p : nnrat} (hq : 0 ≤ q) :

q.to_nnrat < p ↔ q < ↑p

theorem rat.lt_to_nnrat_iff_coe_lt {p : ℚ} {q : nnrat} :

q < p.to_nnrat ↔ ↑q < p

@[simp]

theorem rat.to_nnrat_bit0 {q : ℚ} (hq : 0 ≤ q) :

(bit0 q).to_nnrat = bit0 q.to_nnrat

@[simp]

theorem rat.to_nnrat_bit1 {q : ℚ} (hq : 0 ≤ q) :

(bit1 q).to_nnrat = bit1 q.to_nnrat

theorem rat.to_nnrat_mul {p q : ℚ} (hp : 0 ≤ p) :

(p * q).to_nnrat = p.to_nnrat * q.to_nnrat

theorem rat.to_nnrat_inv (q : ℚ) :

q⁻¹.to_nnrat = (q.to_nnrat)⁻¹

theorem rat.to_nnrat_div {p q : ℚ} (hp : 0 ≤ p) :

(p / q).to_nnrat = p.to_nnrat / q.to_nnrat

theorem rat.to_nnrat_div' {p q : ℚ} (hq : 0 ≤ q) :

(p / q).to_nnrat = p.to_nnrat / q.to_nnrat

def rat.nnabs (x : ℚ) :

The absolute value on ℚ as a map to ℚ≥0.

Equations

rat.nnabs x = ⟨|x|, _⟩

@[simp, norm_cast]

theorem rat.coe_nnabs (x : ℚ) :

↑(rat.nnabs x) = |x|

Numerator and denominator #

def nnrat.num (q : nnrat) :

The numerator of a nonnegative rational.

Equations

q.num = ↑q.num.nat_abs

def nnrat.denom (q : nnrat) :

The denominator of a nonnegative rational.

Equations

q.denom = ↑q.denom

@[simp]

theorem nnrat.nat_abs_num_coe {q : nnrat} :

↑q.num.nat_abs = q.num

@[simp]

theorem nnrat.denom_coe {q : nnrat} :

↑q.denom = q.denom

theorem nnrat.ext_num_denom {p q : nnrat} (hn : p.num = q.num) (hd : p.denom = q.denom) :

p = q

theorem nnrat.ext_num_denom_iff {p q : nnrat} :

p = q ↔ p.num = q.num ∧ p.denom = q.denom

@[simp]

theorem nnrat.num_div_denom (q : nnrat) :

↑(q.num) / ↑(q.denom) = q

@[protected]

def nnrat.rec {α : nnrat → Sort u_1} (h : Π (m n : ℕ), α (↑m / ↑n)) (q : nnrat) :

α q

A recursor for nonnegative rationals in terms of numerators and denominators.

Equations

nnrat.rec h q = eq.rec (h q.num q.denom) _