Documentation

Mathlib.Data.ENat.Basic

Definition and basic properties of extended natural numbers #

In this file we define ENat (notation: ℕ∞) to be WithTop and prove some basic lemmas about this type.

Implementation details #

There are two natural coercions from to WithTop ℕ = ENat: WithTop.some and Nat.cast. In Lean 3, this difference was hidden in typeclass instances. Since these instances were definitionally equal, we did not duplicate generic lemmas about WithTop α and WithTop.some coercion for ENat and Nat.cast coercion. If you need to apply a lemma about WithTop, you may either rewrite back and forth using ENat.some_eq_coe, or restate the lemma for ENat.

def ENat :

Extended natural numbers ℕ∞ = WithTop.

Equations
Instances For

    Extended natural numbers ℕ∞ = WithTop.

    Equations
    Instances For
      Equations
      Equations
      instance ENat.instIsWellOrderLt :
      IsWellOrder ℕ∞ fun (x x_1 : ℕ∞) => x < x_1
      Equations
      @[simp]
      theorem ENat.some_eq_coe :
      WithTop.some = Nat.cast

      Lemmas about WithTop expect (and can output) WithTop.some but the normal form for coercion ℕ → ℕ∞ is Nat.cast.

      theorem ENat.coe_zero :
      0 = 0
      theorem ENat.coe_one :
      1 = 1
      theorem ENat.coe_add (m : ) (n : ) :
      (m + n) = m + n
      @[simp]
      theorem ENat.coe_sub (m : ) (n : ) :
      (m - n) = m - n
      @[simp]
      theorem ENat.coe_mul (m : ) (n : ) :
      (m * n) = m * n
      @[simp]
      theorem ENat.mul_top {m : ℕ∞} (hm : m 0) :
      @[simp]
      theorem ENat.top_mul {m : ℕ∞} (hm : m 0) :
      theorem ENat.top_pow {n : } (n_pos : 0 < n) :
      instance ENat.canLift :
      CanLift ℕ∞ Nat.cast fun (x : ℕ∞) => x
      Equations

      Conversion of ℕ∞ to sending to 0.

      Equations
      Instances For

        Homomorphism from ℕ∞ to sending to 0.

        Equations
        Instances For
          theorem ENat.toNatHom_apply (n : ) :
          ENat.toNatHom n = (n).toNat
          @[simp]
          theorem ENat.toNat_coe (n : ) :
          (n).toNat = n
          @[simp]
          theorem ENat.toNat_ofNat (n : ) [n.AtLeastTwo] :
          (OfNat.ofNat n).toNat = n
          @[simp]
          theorem ENat.toNat_top :
          .toNat = 0
          @[simp]
          theorem ENat.toNat_eq_zero {n : ℕ∞} :
          n.toNat = 0 n = 0 n =
          def ENat.recTopCoe {C : ℕ∞Sort u_1} (top : C ) (coe : (a : ) → C a) (n : ℕ∞) :
          C n

          Recursor for ENat using the preferred forms and ↑a.

          Equations
          Instances For
            @[simp]
            theorem ENat.recTopCoe_top {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
            @[simp]
            theorem ENat.recTopCoe_coe {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) (x : ) :
            ENat.recTopCoe d f x = f x
            @[simp]
            theorem ENat.recTopCoe_zero {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
            ENat.recTopCoe d f 0 = f 0
            @[simp]
            theorem ENat.recTopCoe_one {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) :
            ENat.recTopCoe d f 1 = f 1
            @[simp]
            theorem ENat.recTopCoe_ofNat {C : ℕ∞Sort u_1} (d : C ) (f : (a : ) → C a) (x : ) [x.AtLeastTwo] :
            @[simp]
            theorem ENat.top_ne_coe (a : ) :
            a
            @[simp]
            theorem ENat.top_ne_ofNat (a : ) [a.AtLeastTwo] :
            @[simp]
            @[simp]
            @[simp]
            theorem ENat.coe_ne_top (a : ) :
            a
            @[simp]
            theorem ENat.ofNat_ne_top (a : ) [a.AtLeastTwo] :
            @[simp]
            @[simp]
            @[simp]
            theorem ENat.top_sub_coe (a : ) :
            - a =
            @[simp]
            @[simp]
            theorem ENat.top_sub_ofNat (a : ) [a.AtLeastTwo] :
            @[simp]
            theorem ENat.sub_top (a : ℕ∞) :
            a - = 0
            @[simp]
            theorem ENat.coe_toNat_eq_self {n : ℕ∞} :
            n.toNat = n n
            theorem ENat.coe_toNat {n : ℕ∞} :
            n n.toNat = n

            Alias of the reverse direction of ENat.coe_toNat_eq_self.

            theorem ENat.coe_toNat_le_self (n : ℕ∞) :
            n.toNat n
            theorem ENat.toNat_add {m : ℕ∞} {n : ℕ∞} (hm : m ) (hn : n ) :
            (m + n).toNat = m.toNat + n.toNat
            theorem ENat.toNat_sub {n : ℕ∞} (hn : n ) (m : ℕ∞) :
            (m - n).toNat = m.toNat - n.toNat
            theorem ENat.toNat_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
            m.toNat = n m = n
            theorem ENat.toNat_le_of_le_coe {m : ℕ∞} {n : } (h : m n) :
            m.toNat n
            theorem ENat.toNat_le_toNat {m : ℕ∞} {n : ℕ∞} (h : m n) (hn : n ) :
            m.toNat n.toNat
            @[simp]
            theorem ENat.succ_def (m : ℕ∞) :
            Order.succ m = m + 1
            theorem ENat.add_one_le_of_lt {m : ℕ∞} {n : ℕ∞} (h : m < n) :
            m + 1 n
            theorem ENat.add_one_le_iff {m : ℕ∞} {n : ℕ∞} (hm : m ) :
            m + 1 n m < n
            theorem ENat.one_le_iff_pos {n : ℕ∞} :
            1 n 0 < n
            theorem ENat.lt_one_iff_eq_zero {n : ℕ∞} :
            n < 1 n = 0
            theorem ENat.le_of_lt_add_one {m : ℕ∞} {n : ℕ∞} (h : m < n + 1) :
            m n
            theorem ENat.le_coe_iff {n : ℕ∞} {k : } :
            n k ∃ (n₀ : ), n = n₀ n₀ k
            theorem ENat.nat_induction {P : ℕ∞Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ (n : ), P nP n.succ) (htop : (∀ (n : ), P n)P ) :
            P a