HepLean Documentation

Mathlib.Data.NNRat.Defs

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 Semifield here. See Mathlib.Algebra.Field.Rat 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 Rat.instZeroLEOneClass :

ZeroLEOneClass ℚ

Equations

Rat.instZeroLEOneClass = ⋯

instance Rat.instPosMulMono :

Equations

Rat.instPosMulMono = ⋯

instance NNRat.instNontrivial :

Nontrivial ℚ≥0

Equations

NNRat.instNontrivial = ⋯

instance NNRat.instOrderBot :

OrderBot ℚ≥0

Equations

NNRat.instOrderBot = OrderBot.mk NNRat.instOrderBot.proof_1

@[simp]

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

↑q = ↑q

instance NNRat.instCharZero :

CharZero ℚ≥0

Equations

NNRat.instCharZero = ⋯

instance NNRat.canLift :

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

Equations

NNRat.canLift = ⋯

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

p = q ↔ ↑p = ↑q

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.ne_iff {x : ℚ≥0} {y : ℚ≥0} :

↑x ≠ ↑y ↔ x ≠ y

@[simp]

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

↑⟨q, hq⟩ = q

theorem NNRat.forall {p : ℚ≥0 → Prop} :

(∀ (q : ℚ≥0), p q) ↔ ∀ (q : ℚ) (hq : 0 ≤ q), p ⟨q, hq⟩

theorem NNRat.exists {p : ℚ≥0 → Prop} :

(∃ (q : ℚ≥0), p q) ↔ ∃ (q : ℚ) (hq : 0 ≤ q), p ⟨q, hq⟩

def Rat.toNNRat (q : ℚ) :

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

Equations

q.toNNRat = ⟨max q 0, ⋯⟩

Instances For

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

↑q.toNNRat = q

theorem Rat.le_coe_toNNRat (q : ℚ) :

q ≤ ↑q.toNNRat

@[simp]

theorem NNRat.coe_nonneg (q : ℚ≥0) :

0 ≤ ↑q

@[simp]

theorem NNRat.coe_zero :

↑0 = 0

@[simp]

theorem NNRat.num_zero :

NNRat.num 0 = 0

@[simp]

theorem NNRat.den_zero :

NNRat.den 0 = 1

@[simp]

theorem NNRat.coe_one :

↑1 = 1

@[simp]

theorem NNRat.num_one :

NNRat.num 1 = 1

@[simp]

theorem NNRat.den_one :

NNRat.den 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) :

(↑q).toNNRat = q

@[simp]

theorem NNRat.toNNRat_coe_nat (n : ℕ) :

(↑n).toNNRat = ↑n

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

Instances For

def NNRat.coeHom :

ℚ≥0 →+* ℚ

Coercion ℚ≥0 → ℚ as a RingHom.

Equations

NNRat.coeHom = { toFun := NNRat.cast, 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_natCast (n : ℕ) :

⟨↑n, ⋯⟩ = ↑n

@[deprecated NNRat.mk_natCast]

theorem NNRat.mk_coe_nat (n : ℕ) :

⟨↑n, ⋯⟩ = ↑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 = (↑p - ↑q).toNNRat

@[simp]

theorem NNRat.abs_coe (q : ℚ≥0) :

|↑q| = ↑q

@[simp]

theorem NNRat.nonpos_iff_eq_zero (q : ℚ≥0) :

q ≤ 0 ↔ q = 0

@[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 < q.toNNRat ↔ 0 < q

@[simp]

theorem Rat.toNNRat_eq_zero {q : ℚ} :

q.toNNRat = 0 ↔ q ≤ 0

theorem Rat.toNNRat_of_nonpos {q : ℚ} :

q ≤ 0 → q.toNNRat = 0

Alias of the reverse direction of Rat.toNNRat_eq_zero.

@[simp]

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

q.toNNRat ≤ p.toNNRat ↔ q ≤ p

@[simp]

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

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

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

q.toNNRat < p.toNNRat ↔ q < p

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

q.toNNRat < p.toNNRat ↔ q < p

@[simp]

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

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

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

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

theorem Rat.toNNRat_le_iff_le_coe {q : ℚ} {p : ℚ≥0} :

q.toNNRat ≤ p ↔ q ≤ ↑p

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

q ≤ p.toNNRat ↔ ↑q ≤ p

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

q ≤ p.toNNRat ↔ ↑q ≤ p

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

q.toNNRat < p ↔ q < ↑p

theorem Rat.lt_toNNRat_iff_coe_lt {p : ℚ} {q : ℚ≥0} :

q < p.toNNRat ↔ ↑q < p

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

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

def Rat.nnabs (x : ℚ) :

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

Equations

Rat.nnabs x = ⟨|x|, ⋯⟩

Instances For

@[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} :

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

q.num.Coprime q.den

@[simp]

theorem NNRat.num_natCast (n : ℕ) :

(↑n).num = n

@[simp]

theorem NNRat.den_natCast (n : ℕ) :

(↑n).den = 1

@[simp]

theorem NNRat.num_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat n).num = OfNat.ofNat n

@[simp]

theorem NNRat.den_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat 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 : ℕ) :

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

See also Rat.divInt and mkRat.

Equations

NNRat.divNat n d = ⟨Rat.divInt ↑n ↑d, ⋯⟩

Instances For

@[simp]

theorem NNRat.coe_divNat (n : ℕ) (d : ℕ) :

↑(NNRat.divNat n d) = Rat.divInt ↑n ↑d

theorem NNRat.mk_divInt (n : ℕ) (d : ℕ) :

⟨Rat.divInt ↑n ↑d, ⋯⟩ = 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.divNat_zero (n : ℕ) :

NNRat.divNat n 0 = 0

@[simp]

theorem NNRat.num_divNat_den (q : ℚ≥0) :

NNRat.divNat q.num q.den = q

theorem NNRat.natCast_eq_divNat (n : ℕ) :

↑n = NNRat.divNat n 1

theorem NNRat.divNat_mul_divNat (n₁ : ℕ) (n₂ : ℕ) {d₁ : ℕ} {d₂ : ℕ} (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) :

NNRat.divNat n₁ d₁ * NNRat.divNat n₂ d₂ = NNRat.divNat (n₁ * n₂) (d₁ * d₂)

theorem NNRat.divNat_mul_left {a : ℕ} (ha : a ≠ 0) (n : ℕ) (d : ℕ) :

NNRat.divNat (a * n) (a * d) = NNRat.divNat n d

theorem NNRat.divNat_mul_right {a : ℕ} (ha : a ≠ 0) (n : ℕ) (d : ℕ) :

NNRat.divNat (n * a) (d * a) = NNRat.divNat n d

@[simp]

theorem NNRat.mul_den_eq_num (q : ℚ≥0) :

q * ↑q.den = ↑q.num

@[simp]

theorem NNRat.den_mul_eq_num (q : ℚ≥0) :

↑q.den * q = ↑q.num

def NNRat.numDenCasesOn {C : ℚ≥0 → Sort u} (q : ℚ≥0) (H : (n d : ℕ) → d ≠ 0 → n.Coprime 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

q.numDenCasesOn H = ⋯.mpr (H q.num q.den ⋯ ⋯)

Instances For

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)

theorem NNRat.lt_def {p : ℚ≥0} {q : ℚ≥0} :

p < q ↔ p.num * q.den < q.num * p.den

theorem NNRat.le_def {p : ℚ≥0} {q : ℚ≥0} :

p ≤ q ↔ p.num * q.den ≤ q.num * p.den