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.

instance ENat.instOrderBot : OrderBot ℕ∞

Equations

• ENat.instOrderBot = WithTop.orderBot

instance ENat.instOrderTop : OrderTop ℕ∞

Equations

• ENat.instOrderTop = WithTop.orderTop

instance ENat.instOrderedSub : OrderedSub ℕ∞

Equations

• ENat.instOrderedSub = ⋯

instance ENat.instSuccOrder : SuccOrder ℕ∞

Equations

• ENat.instSuccOrder = inferInstanceAs (SuccOrder (WithTop ℕ))

instance ENat.instWellFoundedLT : WellFoundedLT ℕ∞

Equations

• ENat.instWellFoundedLT = ⋯

instance ENat.instCharZero : CharZero ℕ∞

Equations

• ENat.instCharZero = ⋯

instance ENat.instIsWellOrderLt : IsWellOrder ℕ∞ fun (x1 x2 : ℕ∞) => x1 < x2

Equations

• ENat.instIsWellOrderLt = ⋯

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

instance ENat.instSuccAddOrder : SuccAddOrder ℕ∞

Equations

• ENat.instSuccAddOrder = SuccAddOrder.mk ENat.instSuccAddOrder.proof_1

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) : m * ⊤ = ⊤

@[simp]

theorem ENat.top_mul {m : ℕ∞} (hm : m ≠ 0) : ⊤ * m = ⊤

theorem ENat.top_pow {n : ℕ} (n_pos : 0 < n) : ⊤ ^ n = ⊤

instance ENat.canLift : CanLift ℕ∞ ℕ Nat.cast fun (x : ℕ∞) => x ≠ ⊤

Equations

• ENat.canLift = ⋯

instance ENat.instWellFoundedRelation : WellFoundedRelation ℕ∞

Equations

• ENat.instWellFoundedRelation = { rel := fun (x1 x2 : ℕ∞) => x1 < x2, wf := ENat.instWellFoundedRelation.proof_1 }

def ENat.toNat : ℕ∞ → ℕ

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations

• ENat.toNat = WithTop.untop' 0

def ENat.toNatHom : ℕ∞ →*₀ ℕ

Homomorphism from ℕ∞ to ℕ sending ∞ to 0.

Equations

• ENat.toNatHom = { toFun := ENat.toNat, map_zero' := ENat.toNatHom.proof_1, map_one' := ENat.toNatHom.proof_2, map_mul' := ENat.toNatHom.proof_3 }

@[simp]

theorem ENat.coe_toNatHom : ⇑ENat.toNatHom = ENat.toNat

theorem ENat.toNatHom_apply (n : ℕ) : ENat.toNatHom ↑n = (↑n).toNat

@[simp]

theorem ENat.toNat_coe (n : ℕ) : (↑n).toNat = n

@[simp]

theorem ENat.toNat_zero : ENat.toNat 0 = 0

@[simp]

theorem ENat.toNat_one : ENat.toNat 1 = 1

@[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] : ENat.recTopCoe d f (OfNat.ofNat x) = f (OfNat.ofNat x)

@[simp]

theorem ENat.top_ne_coe (a : ℕ) : ⊤ ≠ ↑a

@[simp]

theorem ENat.top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ ≠ OfNat.ofNat a

@[simp]

theorem ENat.top_ne_zero : ⊤ ≠ 0

@[simp]

theorem ENat.top_ne_one : ⊤ ≠ 1

@[simp]

theorem ENat.coe_ne_top (a : ℕ) : ↑a ≠ ⊤

@[simp]

theorem ENat.ofNat_ne_top (a : ℕ) [a.AtLeastTwo] : OfNat.ofNat a ≠ ⊤

@[simp]

theorem ENat.zero_ne_top : 0 ≠ ⊤

@[simp]

theorem ENat.one_ne_top : 1 ≠ ⊤

@[simp]

theorem ENat.top_sub_coe (a : ℕ) : ⊤ - ↑a = ⊤

@[simp]

theorem ENat.top_sub_one : ⊤ - 1 = ⊤

@[simp]

theorem ENat.top_sub_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ - OfNat.ofNat a = ⊤

@[simp]

theorem ENat.top_pos : 0 < ⊤

@[deprecated ENat.top_pos]

theorem ENat.zero_lt_top : 0 < ⊤

Alias of ENat.top_pos.

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.one_le_iff_ne_zero {n : ℕ∞} : 1 ≤ n ↔ n ≠ 0

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 ↑n → P ↑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 ≠ ↑⊤

theorem ENat.one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} : 1 ≤ n ↔ n ≠ 0

theorem ENat.add_one_pos {n : ℕ∞} : 0 < n + 1

theorem ENat.add_lt_add_iff_right {m : ℕ∞} {n : ℕ∞} {k : ℕ∞} (h : k ≠ ⊤) : n + k < m + k ↔ n < m

theorem ENat.add_lt_add_iff_left {m : ℕ∞} {n : ℕ∞} {k : ℕ∞} (h : k ≠ ⊤) : k + n < k + m ↔ n < m