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_natCast, or restate the lemma for ENat.

TODO #

Unify ENat.add_iSup/ENat.iSup_add with ENNReal.add_iSup/ENNReal.iSup_add. The key property of ENat and ENNReal we are using is that all a are either absorbing for addition (a + b = a for all b), or that it's order-cancellable (a + b ≤ a + c → b ≤ c for all b, c), and similarly for multiplication.

@[instance_reducible]

instance instBotENat :

Equations

instBotENat = { bot := instBotENat._aux_1 }

@[instance_reducible]

instance instLTENat :

Equations

instLTENat = { lt := instLTENat._aux_1 }

@[instance_reducible]

instance instLinearOrderENat :

LinearOrder ℕ∞

Equations

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

@[instance_reducible]

instance instAddENat :

Equations

instAddENat = { add := instAddENat._aux_1 }

@[instance_reducible]

instance instOrderBotENat :

OrderBot ℕ∞

Equations

instOrderBotENat = { toBot := instBotENat, bot_le := instOrderBotENat._proof_1 }

instance instZeroLEOneClassENat :

ZeroLEOneClass ℕ∞

@[instance_reducible]

instance instSubENat :

Equations

instSubENat = { sub := instSubENat._aux_1 }

@[instance_reducible]

instance instLEENat :

Equations

instLEENat = { le := instLEENat._aux_1 }

@[instance_reducible]

instance instPreorderENat :

Preorder ℕ∞

Equations

instPreorderENat = { toLE := instLEENat, toLT := instLTENat, le_refl := instPreorderENat._proof_1, le_trans := instPreorderENat._proof_2, lt_iff_le_not_ge := instPreorderENat._proof_3 }

@[instance_reducible]

instance instOneENat :

Equations

instOneENat = { one := instOneENat._aux_1 }

@[instance_reducible]

instance instZeroENat :

Equations

instZeroENat = { zero := instZeroENat._aux_1 }

@[instance_reducible]

instance instOrderTopENat :

OrderTop ℕ∞

Equations

instOrderTopENat = { toTop := instTopENat, le_top := instOrderTopENat._proof_1 }

instance instWellFoundedLTENat :

WellFoundedLT ℕ∞

instance instNontrivialENat :

Nontrivial ℕ∞

@[simp]

theorem ENat.some_eq_natCast :

WithTop.some = Nat.cast

Lemmas about WithTop expect (and can output) WithTop.some but the normal form for coercion ℕ → ℕ∞ is Nat.cast.

@[deprecated ENat.some_eq_natCast (since := "2026-07-17")]

theorem ENat.some_eq_coe :

WithTop.some = Nat.cast

Alias of ENat.some_eq_natCast.

Lemmas about WithTop expect (and can output) WithTop.some but the normal form for coercion ℕ → ℕ∞ is Nat.cast.

theorem ENat.natCast_inj {a b : ℕ} :

↑a = ↑b ↔ a = b

@[deprecated ENat.natCast_inj (since := "2026-07-17")]

theorem ENat.coe_inj {a b : ℕ} :

↑a = ↑b ↔ a = b

Alias of ENat.natCast_inj.

theorem ENat.natCast_zero :

↑0 = 0

@[deprecated ENat.natCast_zero (since := "2026-07-17")]

theorem ENat.coe_zero :

↑0 = 0

Alias of ENat.natCast_zero.

theorem ENat.natCast_one :

↑1 = 1

@[deprecated ENat.natCast_one (since := "2026-07-17")]

theorem ENat.coe_one :

↑1 = 1

Alias of ENat.natCast_one.

theorem ENat.natCast_add (m n : ℕ) :

↑(m + n) = ↑m + ↑n

@[deprecated ENat.natCast_add (since := "2026-07-17")]

theorem ENat.coe_add (m n : ℕ) :

↑(m + n) = ↑m + ↑n

Alias of ENat.natCast_add.

@[simp]

theorem ENat.natCast_sub (m n : ℕ) :

↑(m - n) = ↑m - ↑n

@[deprecated ENat.natCast_sub (since := "2026-07-17")]

theorem ENat.coe_sub (m n : ℕ) :

↑(m - n) = ↑m - ↑n

Alias of ENat.natCast_sub.

@[simp]

theorem ENat.natCast_lt_top (n : ℕ) :

↑n < ⊤

@[deprecated ENat.natCast_lt_top (since := "2026-07-17")]

theorem ENat.coe_lt_top (n : ℕ) :

↑n < ⊤

Alias of ENat.natCast_lt_top.

def ENat.lift (x : ℕ∞) (h : x < ⊤) :

Convert a ℕ∞ to a ℕ using a proof that it is not infinite.

Equations

x.lift h = WithTop.untop x ⋯

Instances For

@[simp]

theorem ENat.natCast_lift (x : ℕ∞) (h : x < ⊤) :

↑(x.lift h) = x

@[deprecated ENat.natCast_lift (since := "2026-07-17")]

theorem ENat.coe_lift (x : ℕ∞) (h : x < ⊤) :

↑(x.lift h) = x

Alias of ENat.natCast_lift.

@[simp]

theorem ENat.lift_natCast (n : ℕ) :

(↑n).lift ⋯ = n

@[simp]

theorem ENat.lift_lt_iff {x : ℕ∞} {h : x < ⊤} {n : ℕ} :

x.lift h < n ↔ x < ↑n

@[simp]

theorem ENat.lift_le_iff {x : ℕ∞} {h : x < ⊤} {n : ℕ} :

x.lift h ≤ n ↔ x ≤ ↑n

@[simp]

theorem ENat.lt_lift_iff {x : ℕ} {n : ℕ∞} {h : n < ⊤} :

x < n.lift h ↔ ↑x < n

@[simp]

theorem ENat.le_lift_iff {x : ℕ} {n : ℕ∞} {h : n < ⊤} :

x ≤ n.lift h ↔ ↑x ≤ n

@[deprecated ENat.lift_natCast (since := "2026-07-17")]

theorem ENat.lift_coe (n : ℕ) :

(↑n).lift ⋯ = n

Alias of ENat.lift_natCast.

@[simp]

theorem ENat.lift_zero :

lift 0 ⋯ = 0

@[simp]

theorem ENat.lift_one :

lift 1 ⋯ = 1

@[simp]

theorem ENat.lift_ofNat (n : ℕ) [n.AtLeastTwo] :

(OfNat.ofNat n).lift ⋯ = OfNat.ofNat n

@[simp]

theorem ENat.add_lt_top {a b : ℕ∞} :

a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

@[simp]

theorem ENat.add_eq_top {a b : ℕ∞} :

a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

instance ENat.canLift :

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

@[instance_reducible]

instance ENat.instWellFoundedRelation :

WellFoundedRelation ℕ∞

Equations

ENat.instWellFoundedRelation = WellFoundedLT.toWellFoundedRelation

def ENat.toNat :

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations

ENat.toNat = WithTop.untopD 0

Instances For

@[simp]

theorem ENat.toNat_natCast (n : ℕ) :

(↑n).toNat = n

@[deprecated ENat.toNat_natCast (since := "2026-07-17")]

theorem ENat.toNat_coe (n : ℕ) :

(↑n).toNat = n

Alias of ENat.toNat_natCast.

@[simp]

theorem ENat.toNat_zero :

@[simp]

theorem ENat.toNat_one :

@[simp]

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

(OfNat.ofNat n).toNat = n

@[simp]

theorem ENat.toNat_top :

@[simp]

theorem ENat.toNat_eq_zero {n : ℕ∞} :

n.toNat = 0 ↔ n = 0 ∨ n = ⊤

theorem ENat.toNat_pos {n : ℕ∞} (hn0 : n ≠ 0) (hxt : n ≠ ⊤) :

theorem ENat.lift_eq_toNat_of_lt_top {x : ℕ∞} (hx : x < ⊤) :

x.lift hx = x.toNat

@[simp]

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

recTopCoe d f 0 = f 0

@[simp]

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

recTopCoe d f 1 = f 1

@[simp]

theorem ENat.recTopCoe_ofNat {C : ℕ∞ → Sort u_1} (d : C ⊤) (f : (a : ℕ) → C ↑a) (x : ℕ) [x.AtLeastTwo] :

recTopCoe d f (OfNat.ofNat x) = f (OfNat.ofNat x)

@[simp]

theorem ENat.top_ne_natCast (a : ℕ) :

⊤ ≠ ↑a

@[deprecated ENat.top_ne_natCast (since := "2026-07-17")]

theorem ENat.top_ne_coe (a : ℕ) :

⊤ ≠ ↑a

Alias of ENat.top_ne_natCast.

@[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.natCast_ne_top (a : ℕ) :

↑a ≠ ⊤

@[deprecated ENat.natCast_ne_top (since := "2026-07-17")]

theorem ENat.coe_ne_top (a : ℕ) :

↑a ≠ ⊤

Alias of ENat.natCast_ne_top.

@[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_natCast (a : ℕ) :

⊤ - ↑a = ⊤

@[deprecated ENat.top_sub_natCast (since := "2026-07-17")]

theorem ENat.top_sub_coe (a : ℕ) :

⊤ - ↑a = ⊤

Alias of ENat.top_sub_natCast.

@[simp]

theorem ENat.top_sub_one :

@[simp]

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

⊤ - OfNat.ofNat a = ⊤

@[simp]

theorem ENat.top_pos :

@[simp]

theorem ENat.one_lt_top :

@[simp]

theorem ENat.sub_top (a : ℕ∞) :

a - ⊤ = 0

theorem ENat.natCast_toNat_le_self (n : ℕ∞) :

↑n.toNat ≤ n

@[deprecated ENat.natCast_toNat_le_self (since := "2026-07-17")]

theorem ENat.coe_toNat_le_self (n : ℕ∞) :

↑n.toNat ≤ n

Alias of ENat.natCast_toNat_le_self.

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.add_le_add_iff_left {m n k : ℕ∞} (h : k ≠ ⊤) :

k + n ≤ k + m ↔ n ≤ m

theorem ENat.add_le_add_iff_right {m n k : ℕ∞} (h : k ≠ ⊤) :

n + k ≤ m + k ↔ n ≤ m

theorem ENat.le_natCast_iff {n : ℕ∞} {k : ℕ} :

n ≤ ↑k ↔ ∃ (n₀ : ℕ ), n = ↑n₀ ∧ n₀ ≤ k

@[deprecated ENat.le_natCast_iff (since := "2026-07-17")]

theorem ENat.le_coe_iff {n : ℕ∞} {k : ℕ} :

n ≤ ↑k ↔ ∃ (n₀ : ℕ ), n = ↑n₀ ∧ n₀ ≤ k

Alias of ENat.le_natCast_iff.

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

theorem ENat.add_lt_add {a b c d : ℕ∞} (hac : a < c) (hbd : b < d) :

a + b < c + d

theorem ENat.add_lt_add_of_le_of_lt {a b c d : ℕ∞} :

a ≠ ⊤ → a ≤ b → c < d → a + c < b + d

theorem ENat.add_lt_add_of_lt_of_le {a b c d : ℕ∞} :

c ≠ ⊤ → a < b → c ≤ d → a + c < b + d

theorem ENat.natCast_lt_natCast {n m : ℕ} :

↑n < ↑m ↔ n < m

@[deprecated ENat.natCast_lt_natCast (since := "2026-07-17")]

theorem ENat.coe_lt_coe {n m : ℕ} :

↑n < ↑m ↔ n < m

Alias of ENat.natCast_lt_natCast.

theorem ENat.natCast_le_natCast {n m : ℕ} :

↑n ≤ ↑m ↔ n ≤ m

@[deprecated ENat.natCast_le_natCast (since := "2026-07-17")]

theorem ENat.coe_le_coe {n m : ℕ} :

↑n ≤ ↑m ↔ n ≤ m

Alias of ENat.natCast_le_natCast.

theorem ENat.nat_induction {motive : ℕ∞ → Prop} (a : ℕ∞) (zero : motive 0) (succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ) (top : (∀ (n : ℕ), motive ↑n) → motive ⊤) :

motive a

theorem ENat.ne_top_iff_exists {n : ℕ∞} :

n ≠ ⊤ ↔ ∃ (m : ℕ ), ↑m = n

theorem ENat.eq_top_iff_forall_ne {n : ℕ∞} :

n = ⊤ ↔ ∀ (m : ℕ), ↑m ≠ n

theorem ENat.forall_ne_top {p : ℕ∞ → Prop} :

(∀ (x : ℕ∞), x ≠ ⊤ → p x) ↔ ∀ (x : ℕ), p ↑x

theorem ENat.exists_ne_top {p : ℕ∞ → Prop} :

(∃ (x : ℕ∞), x ≠ ⊤ ∧ p x) ↔ ∃ (x : ℕ ), p ↑x

theorem ENat.eq_top_iff_forall_gt {n : ℕ∞} :

n = ⊤ ↔ ∀ (m : ℕ), ↑m < n

theorem ENat.eq_top_iff_forall_ge {n : ℕ∞} :

n = ⊤ ↔ ∀ (m : ℕ), ↑m ≤ n

theorem ENat.forall_natCast_le_iff_le {m n : ℕ∞} :

(∀ (a : ℕ), ↑a ≤ m → ↑a ≤ n) ↔ m ≤ n

Version of WithTop.forall_natCast_le_iff_le using Nat.cast rather than WithTop.some.

theorem ENat.eq_of_forall_natCast_le_iff {m n : ℕ∞} (hm : ∀ (a : ℕ), ↑a ≤ m ↔ ↑a ≤ n) :

m = n

Version of WithTop.eq_of_forall_natCast_le_iff using Nat.cast rather than WithTop.some.

theorem ENat.exists_nat_gt {n : ℕ∞} (hn : n ≠ ⊤) :

∃ (m : ℕ ), n < ↑m

@[simp]

theorem ENat.sub_eq_top_iff {a b : ℕ∞} :

a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

theorem ENat.sub_ne_top_iff {a b : ℕ∞} :

a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤

theorem ENat.addLECancellable_of_ne_top {a : ℕ∞} :

a ≠ ⊤ → AddLECancellable a

theorem ENat.addLECancellable_of_lt_top {a : ℕ∞} :

a < ⊤ → AddLECancellable a

theorem ENat.addLECancellable_natCast (a : ℕ) :

AddLECancellable ↑a

@[deprecated ENat.addLECancellable_natCast (since := "2026-07-17")]

theorem ENat.addLECancellable_coe (a : ℕ) :

AddLECancellable ↑a

Alias of ENat.addLECancellable_natCast.

def ENat.map {α : Type u_1} (f : ℕ → α) (k : ℕ∞) :

Specialization of WithTop.map to ENat.

Equations

ENat.map f k = WithTop.map f k

Instances For

@[simp]

theorem ENat.map_top {α : Type u_1} (f : ℕ → α) :

map f ⊤ = ⊤

@[simp]

theorem ENat.map_natCast {α : Type u_1} (f : ℕ → α) (a : ℕ) :

map f ↑a = ↑(f a)

@[deprecated ENat.map_natCast (since := "2026-07-17")]

theorem ENat.map_coe {α : Type u_1} (f : ℕ → α) (a : ℕ) :

map f ↑a = ↑(f a)

Alias of ENat.map_natCast.

@[simp]

theorem ENat.map_zero {α : Type u_1} (f : ℕ → α) :

map f 0 = ↑(f 0)

@[simp]

theorem ENat.map_one {α : Type u_1} (f : ℕ → α) :

map f 1 = ↑(f 1)

@[simp]

theorem ENat.map_ofNat {α : Type u_1} (f : ℕ → α) (n : ℕ) [n.AtLeastTwo] :

map f (OfNat.ofNat n) = ↑(f n)

@[simp]

theorem ENat.map_eq_top_iff {n : ℕ∞} {α : Type u_1} {f : ℕ → α} :

map f n = ⊤ ↔ n = ⊤

@[simp]

theorem ENat.strictMono_map_iff {α : Type u_1} {f : ℕ → α} [Preorder α] :

StrictMono (map f) ↔ StrictMono f

@[simp]

theorem ENat.monotone_map_iff {α : Type u_1} {f : ℕ → α} [Preorder α] :

Monotone (map f) ↔ Monotone f

@[simp]

theorem ENat.map_add {β : Type u_2} {F : Type u_3} [Add β] [FunLike F ℕ β] [AddHomClass F ℕ β] (f : F) (a b : ℕ∞) :

map (⇑f) (a + b) = map (⇑f) a + map (⇑f) b

def OneHom.ENatMap {N : Type u_2} [One N] (f : OneHom ℕ N) :

OneHom ℕ∞ (WithTop N)

A version of ENat.map for OneHoms.

Equations

f.ENatMap = { toFun := ENat.map ⇑f, map_one' := ⋯ }

Instances For

def ZeroHom.ENatMap {N : Type u_2} [Zero N] (f : ZeroHom ℕ N) :

ZeroHom ℕ∞ (WithTop N)

A version of ENat.map for ZeroHoms.

Equations

f.ENatMap = { toFun := ENat.map ⇑f, map_zero' := ⋯ }

Instances For

def AddHom.ENatMap {N : Type u_2} [Add N] (f : ℕ →ₙ+ N) :

ℕ∞ →ₙ+ WithTop N

A version of WithTop.map for AddHoms.

Equations

f.ENatMap = { toFun := ENat.map ⇑f, map_add' := ⋯ }

Instances For

@[simp]

theorem AddHom.ENatMap_apply {N : Type u_2} [Add N] (f : ℕ →ₙ+ N) :

⇑f.ENatMap = ENat.map ⇑f

@[simp]

theorem ENat.WithBot.coe_eq_natCast (n : ℕ) :

↑↑n = ↑n

theorem ENat.WithBot.eq_top_iff_forall_ge {n : WithBot ℕ∞} :

n = ⊤ ↔ ∀ (m : ℕ), ↑m ≤ n