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
      @[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
      theorem ENat.coe_mul (m : ) (n : ) :
      ↑(m * n) = m * n
      instance ENat.canLift :
      CanLift ℕ∞ Nat.cast fun n => n
      Equations

      Conversion of ℕ∞ to sending to 0.

      Equations
      Instances For
        @[simp]
        theorem ENat.toNat_coe (n : ) :
        ENat.toNat n = n
        @[simp]
        def ENat.recTopCoe {C : ℕ∞Sort u_1} (h₁ : C ) (h₂ : (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.top_ne_coe (a : ) :
          a
          @[simp]
          theorem ENat.coe_ne_top (a : ) :
          a
          @[simp]
          theorem ENat.top_sub_coe (a : ) :
          - a =
          theorem ENat.sub_top (a : ℕ∞) :
          a - = 0
          @[simp]
          theorem ENat.coe_toNat_eq_self {n : ℕ∞} :
          ↑(ENat.toNat n) = n n
          theorem ENat.coe_toNat {n : ℕ∞} :
          n ↑(ENat.toNat n) = n

          Alias of the reverse direction of ENat.coe_toNat_eq_self.

          theorem ENat.toNat_add {m : ℕ∞} {n : ℕ∞} (hm : m ) (hn : n ) :
          ENat.toNat (m + n) = ENat.toNat m + ENat.toNat n
          theorem ENat.toNat_sub {n : ℕ∞} (hn : n ) (m : ℕ∞) :
          ENat.toNat (m - n) = ENat.toNat m - ENat.toNat n
          theorem ENat.toNat_eq_iff {m : ℕ∞} {n : } (hn : n 0) :
          ENat.toNat m = n m = n
          @[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.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 ↑(Nat.succ n)) (htop : ((n : ) → P n) → P ) :
          P a