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

def NNRat :

Nonnegative rational numbers.

Equations
Instances For
    Equations
    instance NNRat.canLift :
    CanLift NNRat Subtype.val fun (q : ) => 0 q
    Equations
    theorem NNRat.ext {p : NNRat} {q : NNRat} :
    p = qp = q
    @[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
    theorem NNRat.forall {p : NNRatProp} :
    (∀ (q : NNRat), p q) ∀ (q : ) (hq : 0 q), p { val := q, property := hq }
    theorem NNRat.exists {p : NNRatProp} :
    (∃ (q : NNRat), p q) ∃ (q : ) (hq : 0 q), p { val := q, property := hq }
    def Rat.toNNRat (q : ) :

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

    Equations
    Instances For
      theorem Rat.coe_toNNRat (q : ) (hq : 0 q) :
      (Rat.toNNRat q) = 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_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
      @[simp]
      theorem NNRat.toNNRat_coe (q : NNRat) :
      Rat.toNNRat q = q
      @[simp]
      theorem NNRat.toNNRat_coe_nat (n : ) :
      Rat.toNNRat n = n

      Coercion ℚ≥0 → ℚ as a RingHom.

      Equations
      Instances For
        @[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 = Subtype.val
        @[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]
        @[simp]
        @[simp]
        theorem Rat.toNNRat_pos {q : } :
        0 < Rat.toNNRat q 0 < q
        @[simp]
        theorem Rat.toNNRat_eq_zero {q : } :
        theorem Rat.toNNRat_of_nonpos {q : } :
        q 0Rat.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) :
        @[simp]
        theorem Rat.toNNRat_lt_toNNRat_iff {p : } {q : } (h : 0 < p) :
        @[simp]
        theorem Rat.toNNRat_add {p : } {q : } (hq : 0 q) (hp : 0 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) :
        def Rat.nnabs (x : ) :

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

        Equations
        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
          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