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.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 (x x_1 : ℕ∞) => x < x_1

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.

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

ENat.canLift = ⋯

instance ENat.instWellFoundedRelation :

WellFoundedRelation ℕ∞

Equations

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

def ENat.toNat :

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations

ENat.toNat = WithTop.untop' 0

Instances For

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 }

Instances For

@[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_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 = ⊤

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

@[simp]

theorem ENat.top_ne_one :

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

@[simp]

theorem ENat.one_ne_top :

@[simp]

theorem ENat.top_sub_coe (a : ℕ) :

⊤ - ↑a = ⊤

@[simp]

theorem ENat.top_sub_one :

@[simp]

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

⊤ - OfNat.ofNat a = ⊤

@[simp]

theorem ENat.zero_lt_top :

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

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

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

P a