Documentation

Mathlib.Data.Rat.NNRat

Nonnegative rationals #

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

We also define an instance CanLift ℚ ℚ≥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 occurrences 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.

def NNRat :

Nonnegative rational numbers.

Equations

NNRat = { q : ℚ // 0 ≤ q }

Instances For

instance instOrderedSubNNRatToLEToPreorderToPartialOrderToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifieldToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringInstNNRatSub :

OrderedSub NNRat

Equations

One or more equations did not get rendered due to their size.

instance instDenselyOrderedNNRatToLTToPreorderToPartialOrderToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifield :

DenselyOrdered NNRat

Equations

One or more equations did not get rendered due to their size.

def NNRat.«termℚ≥0» :

Lean.ParserDescr

Equations

NNRat.«termℚ≥0» = Lean.ParserDescr.node `NNRat.termℚ≥0 1024 (Lean.ParserDescr.symbol "ℚ≥0")

Instances For

instance NNRat.instCoeNNRatRat :

Equations

NNRat.instCoeNNRatRat = { coe := Subtype.val }

instance NNRat.canLift :

CanLift ℚ NNRat Subtype.val fun (q : ℚ) => 0 ≤ q

Equations

NNRat.canLift = (_ : CanLift ℚ NNRat Subtype.val fun (q : ℚ) => 0 ≤ q)

theorem NNRat.ext {p : NNRat} {q : NNRat} :

↑p = ↑q → p = q

theorem NNRat.coe_injective :

Function.Injective Subtype.val

@[simp]

theorem NNRat.coe_inj {p : NNRat} {q : NNRat} :

↑p = ↑q ↔ p = q

theorem NNRat.ext_iff {p : NNRat} {q : NNRat} :

p = q ↔ ↑p = ↑q

theorem NNRat.ne_iff {x : NNRat} {y : NNRat} :

↑x ≠ ↑y ↔ x ≠ y

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

↑{ val := q, property := hq } = q

def Rat.toNNRat (q : ℚ) :

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

Equations

Rat.toNNRat q = { val := max q 0, property := (_ : 0 ≤ max q 0) }

Instances For

theorem Rat.coe_toNNRat (q : ℚ) (hq : 0 ≤ q) :

↑(Rat.toNNRat q) = q

theorem Rat.le_coe_toNNRat (q : ℚ) :

q ≤ ↑(Rat.toNNRat q)

@[simp]

theorem NNRat.coe_nonneg (q : NNRat) :

0 ≤ ↑q

@[simp]

theorem NNRat.coe_zero :

↑0 = 0

@[simp]

theorem NNRat.coe_one :

↑1 = 1

@[simp]

theorem NNRat.coe_add (p : NNRat) (q : NNRat) :

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

@[simp]

theorem NNRat.coe_mul (p : NNRat) (q : NNRat) :

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

@[simp]

theorem NNRat.coe_inv (q : NNRat) :

↑q⁻¹ = (↑q)⁻¹

@[simp]

theorem NNRat.coe_div (p : NNRat) (q : NNRat) :

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

@[simp]

theorem NNRat.coe_sub {p : NNRat} {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

theorem NNRat.coe_le_coe {p : NNRat} {q : NNRat} :

↑p ≤ ↑q ↔ p ≤ q

theorem NNRat.coe_lt_coe {p : NNRat} {q : NNRat} :

↑p < ↑q ↔ p < q

@[simp]

theorem NNRat.coe_pos {q : NNRat} :

0 < ↑q ↔ 0 < q

theorem NNRat.coe_mono :

Monotone Subtype.val

theorem NNRat.toNNRat_mono :

Monotone Rat.toNNRat

@[simp]

theorem NNRat.toNNRat_coe (q : NNRat) :

Rat.toNNRat ↑q = q

@[simp]

theorem NNRat.toNNRat_coe_nat (n : ℕ) :

Rat.toNNRat ↑n = ↑n

GaloisInsertion Rat.toNNRat Subtype.val

toNNRat and (↑) : ℚ≥0 → ℚ form a Galois insertion.

Equations

NNRat.gi = GaloisInsertion.monotoneIntro NNRat.coe_mono NNRat.toNNRat_mono Rat.le_coe_toNNRat NNRat.toNNRat_coe

Instances For

def NNRat.coeHom :

NNRat →+* ℚ

Coercion ℚ≥0 → ℚ as a RingHom.

Equations

NNRat.coeHom = { toMonoidHom := { toOneHom := { toFun := Subtype.val, map_one' := NNRat.coe_one }, map_mul' := NNRat.coe_mul }, map_zero' := NNRat.coe_zero, map_add' := NNRat.coe_add }

Instances For

@[simp]

theorem NNRat.coe_natCast (n : ℕ) :

↑↑n = ↑n

@[simp]

theorem NNRat.mk_coe_nat (n : ℕ) :

{ val := ↑n, property := (_ : 0 ≤ ↑n) } = ↑n

instance NNRat.instMulActionNNRatToMonoidToMonoidWithZeroToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifield {α : Type u_1} [MulAction ℚ α] :

MulAction NNRat α

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

Equations

One or more equations did not get rendered due to their size.

instance NNRat.instDistribMulActionNNRatToMonoidToMonoidWithZeroToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifieldToAddMonoid {α : Type u_1} [AddCommMonoid α] [DistribMulAction ℚ α] :

DistribMulAction NNRat α

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

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem NNRat.coe_coeHom :

⇑NNRat.coeHom = Subtype.val

@[simp]

theorem NNRat.coe_indicator {α : Type u_1} (s : Set α) (f : α → NNRat) (a : α) :

↑(Set.indicator s f a) = Set.indicator s (fun (x : α) => ↑(f x)) a

@[simp]

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

↑(q ^ n) = ↑q ^ n

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

↑(n • q) = n • ↑q

theorem NNRat.bddAbove_coe {s : Set NNRat} :

BddAbove (Subtype.val '' s) ↔ BddAbove s

theorem NNRat.bddBelow_coe (s : Set NNRat) :

BddBelow (Subtype.val '' s)

@[simp]

theorem NNRat.coe_max (x : NNRat) (y : NNRat) :

↑(max x y) = max ↑x ↑y

@[simp]

theorem NNRat.coe_min (x : NNRat) (y : NNRat) :

↑(min x y) = min ↑x ↑y

theorem NNRat.sub_def (p : NNRat) (q : NNRat) :

p - q = Rat.toNNRat (↑p - ↑q)

@[simp]

theorem NNRat.abs_coe (q : NNRat) :

|↑q| = ↑q

@[simp]

theorem Rat.toNNRat_zero :

Rat.toNNRat 0 = 0

@[simp]

theorem Rat.toNNRat_one :

Rat.toNNRat 1 = 1

@[simp]

theorem Rat.toNNRat_pos {q : ℚ} :

0 < Rat.toNNRat q ↔ 0 < q

@[simp]

theorem Rat.toNNRat_eq_zero {q : ℚ} :

Rat.toNNRat q = 0 ↔ q ≤ 0

theorem Rat.toNNRat_of_nonpos {q : ℚ} :

q ≤ 0 → Rat.toNNRat q = 0

Alias of the reverse direction of Rat.toNNRat_eq_zero.

@[simp]

theorem Rat.toNNRat_le_toNNRat_iff {p : ℚ} {q : ℚ} (hp : 0 ≤ p) :

Rat.toNNRat q ≤ Rat.toNNRat p ↔ q ≤ p

@[simp]

theorem Rat.toNNRat_lt_toNNRat_iff' {p : ℚ} {q : ℚ} :

Rat.toNNRat q < Rat.toNNRat p ↔ q < p ∧ 0 < p

theorem Rat.toNNRat_lt_toNNRat_iff {p : ℚ} {q : ℚ} (h : 0 < p) :

Rat.toNNRat q < Rat.toNNRat p ↔ q < p

theorem Rat.toNNRat_lt_toNNRat_iff_of_nonneg {p : ℚ} {q : ℚ} (hq : 0 ≤ q) :

Rat.toNNRat q < Rat.toNNRat p ↔ q < p

@[simp]

theorem Rat.toNNRat_add {p : ℚ} {q : ℚ} (hq : 0 ≤ q) (hp : 0 ≤ p) :

Rat.toNNRat (q + p) = Rat.toNNRat q + Rat.toNNRat p

theorem Rat.toNNRat_add_le {p : ℚ} {q : ℚ} :

Rat.toNNRat (q + p) ≤ Rat.toNNRat q + Rat.toNNRat p

theorem Rat.toNNRat_le_iff_le_coe {q : ℚ} {p : NNRat} :

Rat.toNNRat q ≤ p ↔ q ≤ ↑p

theorem Rat.le_toNNRat_iff_coe_le {p : ℚ} {q : NNRat} (hp : 0 ≤ p) :

q ≤ Rat.toNNRat p ↔ ↑q ≤ p

theorem Rat.le_toNNRat_iff_coe_le' {p : ℚ} {q : NNRat} (hq : 0 < q) :

q ≤ Rat.toNNRat p ↔ ↑q ≤ p

theorem Rat.toNNRat_lt_iff_lt_coe {q : ℚ} {p : NNRat} (hq : 0 ≤ q) :

Rat.toNNRat q < p ↔ q < ↑p

theorem Rat.lt_toNNRat_iff_coe_lt {p : ℚ} {q : NNRat} :

q < Rat.toNNRat p ↔ ↑q < p

theorem Rat.toNNRat_mul {p : ℚ} {q : ℚ} (hp : 0 ≤ p) :

Rat.toNNRat (p * q) = Rat.toNNRat p * Rat.toNNRat q

theorem Rat.toNNRat_inv (q : ℚ) :

Rat.toNNRat q⁻¹ = (Rat.toNNRat q)⁻¹

theorem Rat.toNNRat_div {p : ℚ} {q : ℚ} (hp : 0 ≤ p) :

Rat.toNNRat (p / q) = Rat.toNNRat p / Rat.toNNRat q

theorem Rat.toNNRat_div' {p : ℚ} {q : ℚ} (hq : 0 ≤ q) :

Rat.toNNRat (p / q) = Rat.toNNRat p / Rat.toNNRat q

def Rat.nnabs (x : ℚ) :

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

Equations

Rat.nnabs x = { val := |x|, property := (_ : 0 ≤ |x|) }

Instances For

@[simp]

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 = Int.natAbs (↑q).num

Instances For

def NNRat.den (q : NNRat) :

The denominator of a nonnegative rational.

Equations

q.den = (↑q).den

Instances For

theorem NNRat.num_coe (q : NNRat) :

(↑q).num = ↑q.num

theorem NNRat.natAbs_num_coe {q : NNRat} :

Int.natAbs (↑q).num = q.num

@[simp]

theorem NNRat.den_coe {q : NNRat} :

(↑q).den = q.den

@[simp]

theorem NNRat.num_ne_zero {q : NNRat} :

q.num ≠ 0 ↔ q ≠ 0

@[simp]

theorem NNRat.num_pos {q : NNRat} :

0 < q.num ↔ 0 < q

@[simp]

theorem NNRat.den_pos (q : NNRat) :

0 < q.den

@[simp]

theorem NNRat.num_natCast (n : ℕ) :

(↑n).num = n

@[simp]

theorem NNRat.den_natCast (n : ℕ) :

(↑n).den = 1

theorem NNRat.ext_num_den {p : NNRat} {q : NNRat} (hn : p.num = q.num) (hd : p.den = q.den) :

p = q

theorem NNRat.ext_num_den_iff {p : NNRat} {q : NNRat} :

p = q ↔ p.num = q.num ∧ p.den = q.den

@[simp]

theorem NNRat.num_div_den (q : NNRat) :

↑q.num / ↑q.den = q

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.mpr (_ : α q = α (↑q.num / ↑q.den)) (h q.num q.den)

Instances For