Documentation

Mathlib.Data.Nat.PartENat

Natural numbers with infinity #

The natural numbers and an extra top element . This implementation uses Part as an implementation. Use ℕ∞ instead unless you care about computability.

Main definitions #

The following instances are defined:

There is no additive analogue of MonoidWithZero; if there were then PartENat could be an AddMonoidWithTop.

Implementation details #

PartENat is defined to be Part.

+ and are defined on PartENat, but there is an issue with * because it's not clear what 0 * ⊤ should be. mul is hence left undefined. Similarly ⊤ - ⊤ is ambiguous so there is no - defined on PartENat.

Before the open scoped Classical line, various proofs are made with decidability assumptions. This can cause issues -- see for example the non-simp lemma toWithTopZero proved by rfl, followed by @[simp] lemma toWithTopZero' whose proof uses convert.

Tags #

PartENat, ℕ∞

Type of natural numbers with infinity ()

Equations
Instances For

    The computable embedding ℕ → PartENat.

    This coincides with the coercion coe : ℕ → PartENat, see PartENat.some_eq_natCast.

    Equations
    Instances For
      Equations
      Equations
      Equations
      @[simp]
      theorem PartENat.dom_some (x : ) :
      (↑x).Dom
      theorem PartENat.some_eq_natCast (n : ) :
      n = n
      theorem PartENat.natCast_inj {x : } {y : } :
      x = y x = y

      Alias of Nat.cast_inj specialized to PartENat -

      @[simp]
      theorem PartENat.dom_natCast (x : ) :
      (↑x).Dom
      @[simp]
      theorem PartENat.dom_ofNat (x : ) [x.AtLeastTwo] :
      (OfNat.ofNat x).Dom
      @[simp]
      Equations
      Equations
      Equations
      Equations
      theorem PartENat.le_def (x : PartENat) (y : PartENat) :
      x y ∃ (h : y.Domx.Dom), ∀ (hy : y.Dom), x.get y.get hy
      theorem PartENat.casesOn' {P : PartENatProp} (a : PartENat) :
      P (∀ (n : ), P n)P a
      theorem PartENat.casesOn {P : PartENatProp} (a : PartENat) :
      P (∀ (n : ), P n)P a
      @[simp]
      theorem PartENat.natCast_get {x : PartENat} (h : x.Dom) :
      (x.get h) = x
      @[simp]
      theorem PartENat.get_natCast' (x : ) (h : (↑x).Dom) :
      (↑x).get h = x
      theorem PartENat.get_natCast {x : } :
      (↑x).get = x
      theorem PartENat.coe_add_get {x : } {y : PartENat} (h : (x + y).Dom) :
      (x + y).get h = x + y.get
      @[simp]
      theorem PartENat.get_add {x : PartENat} {y : PartENat} (h : (x + y).Dom) :
      (x + y).get h = x.get + y.get
      @[simp]
      theorem PartENat.get_zero (h : Part.Dom 0) :
      Part.get 0 h = 0
      @[simp]
      theorem PartENat.get_one (h : Part.Dom 1) :
      Part.get 1 h = 1
      @[simp]
      theorem PartENat.get_ofNat' (x : ) [x.AtLeastTwo] (h : (OfNat.ofNat x).Dom) :
      theorem PartENat.get_eq_iff_eq_some {a : PartENat} {ha : a.Dom} {b : } :
      a.get ha = b a = b
      theorem PartENat.get_eq_iff_eq_coe {a : PartENat} {ha : a.Dom} {b : } :
      a.get ha = b a = b
      theorem PartENat.dom_of_le_of_dom {x : PartENat} {y : PartENat} :
      x yy.Domx.Dom
      theorem PartENat.dom_of_le_some {x : PartENat} {y : } (h : x y) :
      x.Dom
      theorem PartENat.dom_of_le_natCast {x : PartENat} {y : } (h : x y) :
      x.Dom
      instance PartENat.decidableLe (x : PartENat) (y : PartENat) [Decidable x.Dom] [Decidable y.Dom] :
      Equations
      theorem PartENat.lt_def (x : PartENat) (y : PartENat) :
      x < y ∃ (hx : x.Dom), ∀ (hy : y.Dom), x.get hx < y.get hy
      theorem PartENat.coe_le_coe {x : } {y : } :
      x y x y

      Alias of Nat.cast_le specialized to PartENat -

      theorem PartENat.coe_lt_coe {x : } {y : } :
      x < y x < y

      Alias of Nat.cast_lt specialized to PartENat -

      @[simp]
      theorem PartENat.get_le_get {x : PartENat} {y : PartENat} {hx : x.Dom} {hy : y.Dom} :
      x.get hx y.get hy x y
      theorem PartENat.le_coe_iff (x : PartENat) (n : ) :
      x n ∃ (h : x.Dom), x.get h n
      theorem PartENat.lt_coe_iff (x : PartENat) (n : ) :
      x < n ∃ (h : x.Dom), x.get h < n
      theorem PartENat.coe_le_iff (n : ) (x : PartENat) :
      n x ∀ (h : x.Dom), n x.get h
      theorem PartENat.coe_lt_iff (n : ) (x : PartENat) :
      n < x ∀ (h : x.Dom), n < x.get h
      theorem PartENat.dom_of_lt {x : PartENat} {y : PartENat} :
      x < yx.Dom
      theorem PartENat.top_eq_none :
      = Part.none
      @[simp]
      theorem PartENat.natCast_lt_top (x : ) :
      x <
      @[simp]
      @[simp]
      @[simp]
      theorem PartENat.ofNat_lt_top (x : ) [x.AtLeastTwo] :
      @[simp]
      theorem PartENat.natCast_ne_top (x : ) :
      x
      @[simp]
      @[simp]
      theorem PartENat.ofNat_ne_top (x : ) [x.AtLeastTwo] :
      theorem PartENat.ne_top_iff {x : PartENat} :
      x ∃ (n : ), x = n
      theorem PartENat.ne_top_of_lt {x : PartENat} {y : PartENat} (h : x < y) :
      theorem PartENat.eq_top_iff_forall_lt (x : PartENat) :
      x = ∀ (n : ), n < x
      theorem PartENat.eq_top_iff_forall_le (x : PartENat) :
      x = ∀ (n : ), n x
      instance PartENat.isTotal :
      IsTotal PartENat fun (x1 x2 : PartENat) => x1 x2
      Equations
      noncomputable instance PartENat.linearOrder :
      Equations
      • One or more equations did not get rendered due to their size.
      noncomputable instance PartENat.lattice :
      Equations
      theorem PartENat.eq_natCast_sub_of_add_eq_natCast {x : PartENat} {y : PartENat} {n : } (h : x + y = n) :
      x = (n - y.get )
      theorem PartENat.add_lt_add_right {x : PartENat} {y : PartENat} {z : PartENat} (h : x < y) (hz : z ) :
      x + z < y + z
      theorem PartENat.add_lt_add_iff_right {x : PartENat} {y : PartENat} {z : PartENat} (hz : z ) :
      x + z < y + z x < y
      theorem PartENat.add_lt_add_iff_left {x : PartENat} {y : PartENat} {z : PartENat} (hz : z ) :
      z + x < z + y x < y
      theorem PartENat.lt_add_iff_pos_right {x : PartENat} {y : PartENat} (hx : x ) :
      x < x + y 0 < y
      theorem PartENat.lt_add_one {x : PartENat} (hx : x ) :
      x < x + 1
      theorem PartENat.le_of_lt_add_one {x : PartENat} {y : PartENat} (h : x < y + 1) :
      x y
      theorem PartENat.add_one_le_of_lt {x : PartENat} {y : PartENat} (h : x < y) :
      x + 1 y
      theorem PartENat.add_one_le_iff_lt {x : PartENat} {y : PartENat} (hx : x ) :
      x + 1 y x < y
      theorem PartENat.coe_succ_le_iff {n : } {e : PartENat} :
      n.succ e n < e
      theorem PartENat.lt_add_one_iff_lt {x : PartENat} {y : PartENat} (hx : x ) :
      x < y + 1 x y
      theorem PartENat.lt_coe_succ_iff_le {x : PartENat} {n : } (hx : x ) :
      x < n.succ x n
      theorem PartENat.add_right_cancel_iff {a : PartENat} {b : PartENat} {c : PartENat} (hc : c ) :
      a + c = b + c a = b
      theorem PartENat.add_left_cancel_iff {a : PartENat} {b : PartENat} {c : PartENat} (ha : a ) :
      a + b = a + c b = c

      Computably converts a PartENat to a ℕ∞.

      Equations
      Instances For
        theorem PartENat.toWithTop_top :
        let_fun this := Part.noneDecidable; .toWithTop =
        @[simp]
        theorem PartENat.toWithTop_top' {h : Decidable .Dom} :
        .toWithTop =
        theorem PartENat.toWithTop_some (n : ) :
        (↑n).toWithTop = n
        theorem PartENat.toWithTop_natCast (n : ) :
        ∀ {x : Decidable (↑n).Dom}, (↑n).toWithTop = n
        @[simp]
        theorem PartENat.toWithTop_natCast' (n : ) :
        ∀ {x : Decidable (↑n).Dom}, (↑n).toWithTop = n
        @[simp]
        theorem PartENat.toWithTop_ofNat (n : ) [n.AtLeastTwo] :
        ∀ {x : Decidable (Part.Dom (OfNat.ofNat n))}, (OfNat.ofNat n).toWithTop = OfNat.ofNat n
        @[simp]
        theorem PartENat.toWithTop_le {x : PartENat} {y : PartENat} [hx : Decidable x.Dom] [hy : Decidable y.Dom] :
        x.toWithTop y.toWithTop x y
        @[simp]
        theorem PartENat.toWithTop_lt {x : PartENat} {y : PartENat} [Decidable x.Dom] [Decidable y.Dom] :
        x.toWithTop < y.toWithTop x < y

        Coercion from ℕ∞ to PartENat.

        Equations
        • none = Part.none
        • (some n) = n
        Instances For
          @[simp]
          @[simp]
          theorem PartENat.ofENat_coe (n : ) :
          n = n
          @[simp]
          theorem PartENat.ofENat_zero :
          0 = 0
          @[simp]
          theorem PartENat.ofENat_one :
          1 = 1
          @[simp]
          theorem PartENat.ofENat_ofNat (n : ) [n.AtLeastTwo] :
          @[simp]
          theorem PartENat.toWithTop_ofENat (n : ℕ∞) :
          ∀ {x : Decidable (↑n).Dom}, (↑n).toWithTop = n
          @[simp]
          theorem PartENat.ofENat_toWithTop (x : PartENat) :
          ∀ {x_1 : Decidable x.Dom}, x.toWithTop = x
          @[simp]
          theorem PartENat.ofENat_le {x : ℕ∞} {y : ℕ∞} :
          x y x y
          @[simp]
          theorem PartENat.ofENat_lt {x : ℕ∞} {y : ℕ∞} :
          x < y x < y
          @[simp]
          theorem PartENat.toWithTop_add {x : PartENat} {y : PartENat} :
          (x + y).toWithTop = x.toWithTop + y.toWithTop
          @[simp]
          theorem PartENat.withTopEquiv_apply (x : PartENat) :
          PartENat.withTopEquiv x = x.toWithTop

          Equiv between PartENat and ℕ∞ (for the order isomorphism see withTopOrderIso).

          Equations
          Instances For
            theorem PartENat.withTopEquiv_top :
            PartENat.withTopEquiv =
            theorem PartENat.withTopEquiv_natCast (n : ) :
            PartENat.withTopEquiv n = n
            theorem PartENat.withTopEquiv_zero :
            PartENat.withTopEquiv 0 = 0
            theorem PartENat.withTopEquiv_one :
            PartENat.withTopEquiv 1 = 1
            theorem PartENat.withTopEquiv_ofNat (n : ) [n.AtLeastTwo] :
            PartENat.withTopEquiv (OfNat.ofNat n) = OfNat.ofNat n
            theorem PartENat.withTopEquiv_le {x : PartENat} {y : PartENat} :
            PartENat.withTopEquiv x PartENat.withTopEquiv y x y
            theorem PartENat.withTopEquiv_lt {x : PartENat} {y : PartENat} :
            PartENat.withTopEquiv x < PartENat.withTopEquiv y x < y

            toWithTop induces an order isomorphism between PartENat and ℕ∞.

            Equations
            Instances For

              toWithTop induces an additive monoid isomorphism between PartENat and ℕ∞.

              Equations
              Instances For
                theorem PartENat.lt_wf :
                WellFounded fun (x1 x2 : PartENat) => x1 < x2
                instance PartENat.isWellOrder :
                IsWellOrder PartENat fun (x1 x2 : PartENat) => x1 < x2
                Equations

                The smallest PartENat satisfying a (decidable) predicate P : ℕ → Prop

                Equations
                Instances For
                  @[simp]
                  theorem PartENat.find_get (P : Prop) [DecidablePred P] (h : (PartENat.find P).Dom) :
                  theorem PartENat.find_dom (P : Prop) [DecidablePred P] (h : ∃ (n : ), P n) :
                  theorem PartENat.lt_find (P : Prop) [DecidablePred P] (n : ) (h : mn, ¬P m) :
                  theorem PartENat.lt_find_iff (P : Prop) [DecidablePred P] (n : ) :
                  n < PartENat.find P mn, ¬P m
                  theorem PartENat.find_le (P : Prop) [DecidablePred P] (n : ) (h : P n) :
                  Equations
                  • One or more equations did not get rendered due to their size.