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.

Equations
Equations
instance ENat.instIsWellOrderLt :
IsWellOrder ℕ∞ fun (x1 x2 : ℕ∞) => x1 < x2
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]
      @[simp]
      @[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 =
      @[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
      @[deprecated Order.add_one_le_of_lt]
      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
      @[deprecated Order.one_le_iff_pos]
      theorem ENat.one_le_iff_pos {n : ℕ∞} :
      1 n 0 < n
      theorem ENat.lt_one_iff_eq_zero {n : ℕ∞} :
      n < 1 n = 0
      @[deprecated Order.le_of_lt_add_one]
      theorem ENat.le_of_lt_add_one {m : ℕ∞} {n : ℕ∞} (h : m < n + 1) :
      m n
      theorem ENat.lt_add_one_iff {m : ℕ∞} {n : ℕ∞} (hm : n ) :
      m < n + 1 m n
      theorem ENat.le_coe_iff {n : ℕ∞} {k : } :
      n k ∃ (n₀ : ), n = n₀ n₀ k
      @[simp]
      theorem ENat.not_lt_zero (n : ℕ∞) :
      ¬n < 0
      @[simp]
      theorem ENat.coe_lt_top (n : ) :
      n <
      theorem ENat.nat_induction {P : ℕ∞Prop} (a : ℕ∞) (h0 : P 0) (hsuc : ∀ (n : ), P nP n.succ) (htop : (∀ (n : ), P n)P ) :
      P a
      theorem ENat.add_one_nat_le_withTop_of_lt {m : } {n : WithTop ℕ∞} (h : m < n) :
      (m + 1) n
      @[simp]
      theorem ENat.coe_top_add_one :
      + 1 =
      @[simp]
      theorem ENat.add_one_eq_coe_top_iff (n : WithTop ℕ∞) :
      n + 1 = n =
      @[simp]
      theorem ENat.nat_ne_coe_top (n : ) :
      n