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.

Instances For

instance instOrderedSubNNRatToLEToPreorderToPartialOrderToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifieldToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringInstNNRatSub :

OrderedSub NNRat

instance instDenselyOrderedNNRatToLTToPreorderToPartialOrderToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifield :

DenselyOrdered NNRat

instance instArchimedeanNNRatToOrderedAddCommMonoidToOrderedSemiringToOrderedCommSemiringInstNNRatCanonicallyOrderedCommSemiring :

Archimedean NNRat

def NNRat.«termℚ≥0» :

Lean.ParserDescr

Instances For

instance NNRat.instCoeNNRatRat :

instance 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.

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.

Instances For

def NNRat.coeHom :

NNRat →+* ℚ

Coercion ℚ≥0 → ℚ as a RingHom.

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.instAlgebraNNRatRatToCommSemiringInstNNRatCanonicallyOrderedCommSemiringSemiring :

Algebra NNRat ℚ

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

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

MulAction NNRat α

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

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

DistribMulAction NNRat α

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

instance NNRat.instModuleNNRatToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldInstNNRatCanonicallyLinearOrderedSemifield {α : Type u_1} [AddCommMonoid α] [Module ℚ α] :

Module NNRat α

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

@[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.coe_list_sum (l : List NNRat) :

↑(List.sum l) = List.sum (List.map Subtype.val l)

theorem NNRat.coe_list_prod (l : List NNRat) :

↑(List.prod l) = List.prod (List.map Subtype.val l)

theorem NNRat.coe_multiset_sum (s : Multiset NNRat) :

↑(Multiset.sum s) = Multiset.sum (Multiset.map Subtype.val s)

theorem NNRat.coe_multiset_prod (s : Multiset NNRat) :

↑(Multiset.prod s) = Multiset.prod (Multiset.map Subtype.val s)

theorem NNRat.coe_sum {α : Type u_1} {s : Finset α} {f : α → NNRat} :

↑(Finset.sum s fun a => f a) = Finset.sum s fun a => ↑(f a)

theorem NNRat.toNNRat_sum_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℚ} (hf : ∀ (a : α), a ∈ s → 0 ≤ f a) :

Rat.toNNRat (Finset.sum s fun a => f a) = Finset.sum s fun a => Rat.toNNRat (f a)

theorem NNRat.coe_prod {α : Type u_1} {s : Finset α} {f : α → NNRat} :

↑(Finset.prod s fun a => f a) = Finset.prod s fun a => ↑(f a)

theorem NNRat.toNNRat_prod_of_nonneg {α : Type u_1} {s : Finset α} {f : α → ℚ} (hf : ∀ (a : α), a ∈ s → 0 ≤ f a) :

Rat.toNNRat (Finset.prod s fun a => f a) = Finset.prod s fun a => Rat.toNNRat (f a)

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.

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.

Instances For

def NNRat.den (q : NNRat) :

The denominator of a nonnegative rational.

Instances For

@[simp]

theorem NNRat.natAbs_num_coe {q : NNRat} :

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

@[simp]

theorem NNRat.den_coe {q : NNRat} :

(↑q).den = NNRat.den q

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

p = q

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

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

@[simp]

theorem NNRat.num_div_den (q : NNRat) :

↑(NNRat.num q) / ↑(NNRat.den q) = 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.

Instances For