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

ℕ∞ = WithTop ℕ

Instances For

def «termℕ∞» :

Lean.ParserDescr

Extended natural numbers ℕ∞ = WithTop ℕ.

Equations

«termℕ∞» = Lean.ParserDescr.node `termℕ∞ 1024 (Lean.ParserDescr.symbol "ℕ∞")

Instances For

instance ENat.instOrderBotENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

OrderBot ℕ∞

Equations

ENat.instOrderBotENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = WithTop.orderBot

instance ENat.instOrderTopENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

OrderTop ℕ∞

Equations

ENat.instOrderTopENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = WithTop.orderTop

instance ENat.instOrderedSubENatToLEToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiringToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToSemiringInstENatSub :

OrderedSub ℕ∞

Equations

One or more equations did not get rendered due to their size.

instance ENat.instSuccOrderENatToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

SuccOrder ℕ∞

Equations

ENat.instSuccOrderENatToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = inferInstanceAs (SuccOrder (WithTop ℕ))

instance ENat.instWellFoundedLTENatToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

WellFoundedLT ℕ∞

Equations

ENat.instWellFoundedLTENatToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = ⋯

instance ENat.instCharZeroENatToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

CharZero ℕ∞

Equations

ENat.instCharZeroENatToAddMonoidWithOneToAddCommMonoidWithOneToNonAssocSemiringToSemiringToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = ⋯

instance ENat.instIsWellOrderENatLtToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :

IsWellOrder ℕ∞ fun (x x_1 : ℕ∞) => x < x_1

Equations

ENat.instIsWellOrderENatLtToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring = ⋯

@[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) :

instance ENat.canLift :

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

Equations

ENat.canLift = ⋯

instance ENat.instWellFoundedRelationENat :

WellFoundedRelation ℕ∞

Equations

ENat.instWellFoundedRelationENat = { rel := fun (x x_1 : ℕ∞) => x < x_1, wf := ENat.instWellFoundedRelationENat.proof_1 }

def ENat.toNat :

ℕ∞ →*₀ ℕ

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations

ENat.toNat = { toZeroHom := { toFun := WithTop.untop' 0, map_zero' := ENat.toNat.proof_1 }, map_one' := ENat.toNat.proof_2, map_mul' := ENat.toNat.proof_3 }

Instances For

@[simp]

theorem ENat.toNat_coe (n : ℕ) :

ENat.toNat ↑n = n

@[simp]

theorem ENat.toNat_ofNat (n : ℕ) [Nat.AtLeastTwo n] :

ENat.toNat (OfNat.ofNat n) = n

@[simp]

theorem ENat.toNat_top :

ENat.toNat ⊤ = 0

@[simp]

theorem ENat.toNat_eq_zero {n : ℕ∞} :

ENat.toNat n = 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

ENat.recTopCoe top coe x = match x with | none => top | some a => coe 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.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 : ℕ) [Nat.AtLeastTwo x] :

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 : ℕ) [Nat.AtLeastTwo a] :

⊤ ≠ OfNat.ofNat a

@[simp]

theorem ENat.coe_ne_top (a : ℕ) :

↑a ≠ ⊤

@[simp]

theorem ENat.ofNat_ne_top (a : ℕ) [Nat.AtLeastTwo a] :

OfNat.ofNat a ≠ ⊤

@[simp]

theorem ENat.top_sub_coe (a : ℕ) :

⊤ - ↑a = ⊤

@[simp]

theorem ENat.top_sub_one :

@[simp]

theorem ENat.top_sub_ofNat (a : ℕ) [Nat.AtLeastTwo a] :

⊤ - OfNat.ofNat a = ⊤

@[simp]

theorem ENat.zero_lt_top :

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