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 ℕ.

Instances For

def «termℕ∞» :

Lean.ParserDescr

Extended natural numbers ℕ∞ = WithTop ℕ.

Instances For

instance ENat.instOrderBotENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

OrderBot ℕ∞

instance ENat.instOrderTopENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

OrderTop ℕ∞

instance ENat.instOrderedSubENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiringToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringInstENatSub :

OrderedSub ℕ∞

instance ENat.instSuccOrderENatToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

SuccOrder ℕ∞

instance ENat.instWellFoundedLTENatToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

WellFoundedLT ℕ∞

instance ENat.instCharZeroENatToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

CharZero ℕ∞

instance ENat.instIsWellOrderENatLtToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

IsWellOrder ℕ∞ fun x x_1 => x < x_1

@[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 ≠ ⊤

instance ENat.instWellFoundedRelationENat :

WellFoundedRelation ℕ∞

def ENat.toNat :

ℕ∞ →*₀ ℕ

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Instances For

@[simp]

theorem ENat.toNat_coe (n : ℕ) :

↑ENat.toNat ↑n = n

@[simp]

theorem ENat.toNat_top :

↑ENat.toNat ⊤ = 0

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.

Instances For

@[simp]

theorem ENat.recTopCoe_top {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) :

ENat.recTopCoe d f ⊤ = d

@[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.coe_toNat_le_self (n : ℕ∞) :

↑(↑ENat.toNat n) ≤ n

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.one_le_iff_ne_zero {n : ℕ∞} :

1 ≤ n ↔ 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 ↑n → P ↑(Nat.succ n)) (htop : ((n : ℕ) → P ↑n) → P ⊤) :

P a