Nonnegative rationals

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

Note that NNRat is not declared as a Field here. See Data.NNRat.Lemmas for that instance.

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.

Huge warning

Whenever you state a lemma about the coercion ℚ≥0 → ℚ, check that Lean inserts NNRat.cast, not Subtype.val. Else your lemma will never apply.

instance NNRat.instOrderedSub : OrderedSub ℚ≥0

Equations

• NNRat.instOrderedSub = ⋯

@[simp]

theorem NNRat.val_eq_cast (q : ℚ≥0) : ↑q = ↑q

instance NNRat.canLift : CanLift ℚ ℚ≥0 NNRat.cast fun (q : ℚ) => 0 ≤ q

Equations

• NNRat.canLift = ⋯

theorem NNRat.ext {p : ℚ≥0} {q : ℚ≥0} : ↑p = ↑q → p = q

theorem NNRat.coe_injective : Function.Injective NNRat.cast

@[simp]

theorem NNRat.coe_inj {p : ℚ≥0} {q : ℚ≥0} : ↑p = ↑q ↔ p = q

theorem NNRat.ext_iff {p : ℚ≥0} {q : ℚ≥0} : p = q ↔ ↑p = ↑q

theorem NNRat.ne_iff {x : ℚ≥0} {y : ℚ≥0} : ↑x ≠ ↑y ↔ x ≠ y

@[simp]

theorem NNRat.coe_mk (q : ℚ) (hq : 0 ≤ q) : ↑{ val := q, property := hq } = q

theorem NNRat.forall {p : ℚ≥0 → Prop} : (∀ (q : ℚ≥0), p q) ↔ ∀ (q : ℚ) (hq : 0 ≤ q), p { val := q, property := hq }

theorem NNRat.exists {p : ℚ≥0 → Prop} : (∃ (q : ℚ≥0), p q) ↔ ∃ (q : ℚ) (hq : 0 ≤ q), p { val := q, property := hq }

def Rat.toNNRat (q : ℚ) : ℚ≥0

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 := ⋯ }

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 : ℚ≥0) : 0 ≤ ↑q

@[simp]

theorem NNRat.coe_zero : ↑0 = 0

@[simp]

theorem NNRat.coe_one : ↑1 = 1

@[simp]

theorem NNRat.coe_add (p : ℚ≥0) (q : ℚ≥0) : ↑(p + q) = ↑p + ↑q

@[simp]

theorem NNRat.coe_mul (p : ℚ≥0) (q : ℚ≥0) : ↑(p * q) = ↑p * ↑q

@[simp]

theorem NNRat.coe_pow (q : ℚ≥0) (n : ℕ) : ↑(q ^ n) = ↑q ^ n

@[simp]

theorem NNRat.num_pow (q : ℚ≥0) (n : ℕ) : (q ^ n).num = q.num ^ n

@[simp]

theorem NNRat.den_pow (q : ℚ≥0) (n : ℕ) : (q ^ n).den = q.den ^ n

@[simp]

theorem NNRat.coe_sub {p : ℚ≥0} {q : ℚ≥0} (h : q ≤ p) : ↑(p - q) = ↑p - ↑q

@[simp]

theorem NNRat.coe_eq_zero {q : ℚ≥0} : ↑q = 0 ↔ q = 0

theorem NNRat.coe_ne_zero {q : ℚ≥0} : ↑q ≠ 0 ↔ q ≠ 0

theorem NNRat.coe_le_coe {p : ℚ≥0} {q : ℚ≥0} : ↑p ≤ ↑q ↔ p ≤ q

theorem NNRat.coe_lt_coe {p : ℚ≥0} {q : ℚ≥0} : ↑p < ↑q ↔ p < q

@[simp]

theorem NNRat.coe_pos {q : ℚ≥0} : 0 < ↑q ↔ 0 < q

theorem NNRat.coe_mono : Monotone NNRat.cast

theorem NNRat.toNNRat_mono : Monotone Rat.toNNRat

@[simp]

theorem NNRat.toNNRat_coe (q : ℚ≥0) : Rat.toNNRat ↑q = q

@[simp]

theorem NNRat.toNNRat_coe_nat (n : ℕ) : Rat.toNNRat ↑n = ↑n

def NNRat.gi : GaloisInsertion Rat.toNNRat NNRat.cast

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

def NNRat.coeHom : ℚ≥0 →+* ℚ

Coercion ℚ≥0 → ℚ as a RingHom.

Equations

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

@[simp]

theorem NNRat.coe_natCast (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem NNRat.mk_natCast (n : ℕ) : { val := ↑n, property := ⋯ } = ↑n

@[deprecated NNRat.mk_natCast]

theorem NNRat.mk_coe_nat (n : ℕ) : { val := ↑n, property := ⋯ } = ↑n

Alias of NNRat.mk_natCast.

@[simp]

theorem NNRat.coe_coeHom : ⇑NNRat.coeHom = NNRat.cast

theorem NNRat.nsmul_coe (q : ℚ≥0) (n : ℕ) : ↑(n • q) = n • ↑q

theorem NNRat.bddAbove_coe {s : Set ℚ≥0} : BddAbove (NNRat.cast '' s) ↔ BddAbove s

theorem NNRat.bddBelow_coe (s : Set ℚ≥0) : BddBelow (NNRat.cast '' s)

@[simp]

theorem NNRat.coe_max (x : ℚ≥0) (y : ℚ≥0) : ↑(max x y) = max ↑x ↑y

@[simp]

theorem NNRat.coe_min (x : ℚ≥0) (y : ℚ≥0) : ↑(min x y) = min ↑x ↑y

theorem NNRat.sub_def (p : ℚ≥0) (q : ℚ≥0) : p - q = Rat.toNNRat (↑p - ↑q)

@[simp]

theorem NNRat.abs_coe (q : ℚ≥0) : |↑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 : ℚ≥0} : Rat.toNNRat q ≤ p ↔ q ≤ ↑p

theorem Rat.le_toNNRat_iff_coe_le {p : ℚ} {q : ℚ≥0} (hp : 0 ≤ p) : q ≤ Rat.toNNRat p ↔ ↑q ≤ p

theorem Rat.le_toNNRat_iff_coe_le' {p : ℚ} {q : ℚ≥0} (hq : 0 < q) : q ≤ Rat.toNNRat p ↔ ↑q ≤ p

theorem Rat.toNNRat_lt_iff_lt_coe {q : ℚ} {p : ℚ≥0} (hq : 0 ≤ q) : Rat.toNNRat q < p ↔ q < ↑p

theorem Rat.lt_toNNRat_iff_coe_lt {p : ℚ} {q : ℚ≥0} : 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

def Rat.nnabs (x : ℚ) : ℚ≥0

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

Equations

• Rat.nnabs x = { val := |x|, property := ⋯ }

@[simp]

theorem Rat.coe_nnabs (x : ℚ) : ↑(Rat.nnabs x) = |x|

Numerator and denominator

theorem NNRat.num_coe (q : ℚ≥0) : (↑q).num = ↑q.num

theorem NNRat.natAbs_num_coe {q : ℚ≥0} : Int.natAbs (↑q).num = q.num

theorem NNRat.den_coe {q : ℚ≥0} : (↑q).den = q.den

@[simp]

theorem NNRat.num_ne_zero {q : ℚ≥0} : q.num ≠ 0 ↔ q ≠ 0

@[simp]

theorem NNRat.num_pos {q : ℚ≥0} : 0 < q.num ↔ 0 < q

@[simp]

theorem NNRat.den_pos (q : ℚ≥0) : 0 < q.den

@[simp]

theorem NNRat.den_ne_zero (q : ℚ≥0) : q.den ≠ 0

theorem NNRat.coprime_num_den (q : ℚ≥0) : Nat.Coprime q.num 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 : ℚ≥0} {q : ℚ≥0} (hn : p.num = q.num) (hd : p.den = q.den) : p = q

theorem NNRat.ext_num_den_iff {p : ℚ≥0} {q : ℚ≥0} : p = q ↔ p.num = q.num ∧ p.den = q.den

def NNRat.divNat (n : ℕ) (d : ℕ) : ℚ≥0

Form the quotient n / d where n d : ℕ.

See also Rat.divInt and mkRat.

Equations

• NNRat.divNat n d = { val := Rat.divInt ↑n ↑d, property := ⋯ }

@[simp]

theorem NNRat.coe_divNat (n : ℕ) (d : ℕ) : ↑(NNRat.divNat n d) = Rat.divInt ↑n ↑d

theorem NNRat.mk_divInt (n : ℕ) (d : ℕ) : { val := Rat.divInt ↑n ↑d, property := ⋯ } = NNRat.divNat n d

theorem NNRat.divNat_inj {n₁ : ℕ} {n₂ : ℕ} {d₁ : ℕ} {d₂ : ℕ} (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : NNRat.divNat n₁ d₁ = NNRat.divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

@[simp]

theorem NNRat.num_divNat_den (q : ℚ≥0) : NNRat.divNat q.num q.den = q

def NNRat.numDenCasesOn {C : ℚ≥0 → Sort u} (q : ℚ≥0) (H : (n d : ℕ) → d ≠ 0 → Nat.Coprime n d → C (NNRat.divNat n d)) : C q

Define a (dependent) function or prove ∀ r : ℚ, p r by dealing with nonnegative rational numbers of the form n / d with d ≠ 0 and n, d coprime.

Equations

• NNRat.numDenCasesOn q H = Eq.mpr ⋯ (H q.num q.den ⋯ ⋯)

theorem NNRat.add_def (q : ℚ≥0) (r : ℚ≥0) : q + r = NNRat.divNat (q.num * r.den + r.num * q.den) (q.den * r.den)

theorem NNRat.mul_def (q : ℚ≥0) (r : ℚ≥0) : q * r = NNRat.divNat (q.num * r.num) (q.den * r.den)