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.

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 instENatZero :

Equations

instENatZero = WithTop.zero

instance instENatCommSemiring :

CommSemiring ℕ∞

Equations

instENatCommSemiring = WithTop.instCommSemiring

instance instENatNontrivial :

Nontrivial ℕ∞

Equations

instENatNontrivial = ⋯

instance instENatLinearOrder :

LinearOrder ℕ∞

Equations

instENatLinearOrder = WithTop.linearOrder

instance instENatBot :

Equations

instENatBot = WithTop.instBot

instance instENatSub :

Equations

instENatSub = WithTop.instSub

instance instENatLinearOrderedAddCommMonoidWithTop :

LinearOrderedAddCommMonoidWithTop ℕ∞

Equations

instENatLinearOrderedAddCommMonoidWithTop = WithTop.linearOrderedAddCommMonoidWithTop

instance instENatWellFoundedRelation :

WellFoundedRelation ℕ∞

Equations

instENatWellFoundedRelation = instWellFoundedRelationOfSizeOf

instance ENat.instIsOrderedRing :

IsOrderedRing ℕ∞

instance ENat.instCanonicallyOrderedAdd :

CanonicallyOrderedAdd ℕ∞

instance ENat.instOrderBot :

OrderBot ℕ∞

Equations

ENat.instOrderBot = WithTop.orderBot

instance ENat.instOrderTop :

OrderTop ℕ∞

Equations

ENat.instOrderTop = WithTop.orderTop

instance ENat.instOrderedSub :

OrderedSub ℕ∞

instance ENat.instSuccOrder :

SuccOrder ℕ∞

Equations

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

instance ENat.instWellFoundedLT :

WellFoundedLT ℕ∞

instance ENat.instCharZero :

CharZero ℕ∞

@[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_inj {a b : ℕ} :

↑a = ↑b ↔ a = b

instance ENat.instSuccAddOrder :

SuccAddOrder ℕ∞

Equations

ENat.instSuccAddOrder = { toSuccOrder := ENat.instSuccOrder, succ_eq_add_one := 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) :

@[simp]

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

theorem ENat.mul_top' {m : ℕ∞} :

m * ⊤ = if m = 0 then 0 else ⊤

A version of mul_top where the RHS is stated as an ite

theorem ENat.top_mul' {m : ℕ∞} :

⊤ * m = if m = 0 then 0 else ⊤

A version of top_mul where the RHS is stated as an ite

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

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 ⋯

@[simp]

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

↑(x.lift h) = x

@[simp]

theorem ENat.lift_coe (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

@[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.lift_add (a b : ℕ∞) (h : a + b < ⊤) :

(a + b).lift h = a.lift ⋯ + b.lift ⋯

instance ENat.canLift :

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

instance ENat.instWellFoundedRelation :

WellFoundedRelation ℕ∞

Equations

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

def ENat.toNat :

Conversion of ℕ∞ to ℕ sending ∞ to 0.

Equations

ENat.toNat = WithTop.untopD 0

def ENat.toNatHom :

ℕ∞ →*₀ ℕ

Homomorphism from ℕ∞ to ℕ sending ∞ to 0.

Equations

ENat.toNatHom = { toFun := ENat.toNat, map_zero' := ENat.toNatHom._proof_10, map_one' := ENat.toNatHom._proof_11, map_mul' := ⋯ }

@[simp]

theorem ENat.coe_toNatHom :

⇑toNatHom = toNat

theorem ENat.toNatHom_apply (n : ℕ) :

toNatHom ↑n = (↑n).toNat

@[simp]

theorem ENat.toNat_coe (n : ℕ) :

(↑n).toNat = n

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

@[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_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.top_pos :

@[deprecated ENat.top_pos (since := "2024-10-22")]

theorem ENat.zero_lt_top :

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.

@[simp]

theorem ENat.toNat_eq_iff_eq_coe (n : ℕ∞) (m : ℕ) [NeZero m] :

n.toNat = m ↔ n = ↑m

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_mul (a b : ℕ∞) :

(a * b).toNat = a.toNat * b.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) :

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_iff {m n : ℕ∞} (hm : m ≠ ⊤) :

m + 1 ≤ n ↔ m < 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.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.coe_lt_coe {n m : ℕ} :

↑n < ↑m ↔ n < m

theorem ENat.coe_le_coe {n m : ℕ} :

↑n ≤ ↑m ↔ n ≤ m

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_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

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

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_coe (a : ℕ) :

AddLECancellable ↑a

theorem ENat.le_sub_of_add_le_left {a b c : ℕ∞} (ha : a ≠ ⊤) :

a + b ≤ c → b ≤ c - a

theorem ENat.sub_sub_cancel {a b : ℕ∞} (h : a ≠ ⊤) (h2 : b ≤ a) :

a - (a - b) = b

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

Function.Injective fun (x : ℕ∞) => x + n

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

Function.Injective fun (x : ℕ∞) => n + x

theorem ENat.mul_left_strictMono {a : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :

StrictMono fun (x : ℕ∞) => a * x

theorem ENat.mul_right_strictMono {a : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :

StrictMono fun (x : ℕ∞) => x * a

@[simp]

theorem ENat.mul_le_mul_left_iff {a x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :

a * x ≤ a * y ↔ x ≤ y

@[simp]

theorem ENat.mul_le_mul_right_iff {a x y : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :

x * a ≤ y * a ↔ x ≤ y

theorem ENat.mul_le_mul_of_le_right {a x y : ℕ∞} (hxy : x ≤ y) (ha : a ≠ 0) (h_top : a ≠ ⊤) :

x * a ≤ y * a

theorem ENat.self_le_mul_right {c : ℕ∞} (a : ℕ∞) (hc : c ≠ 0) :

a ≤ a * c

theorem ENat.self_le_mul_left {c : ℕ∞} (a : ℕ∞) (hc : c ≠ 0) :

a ≤ c * a

theorem ENat.add_one_natCast_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.natCast_ne_coe_top (n : ℕ) :

↑n ≠ ↑⊤

@[deprecated ENat.natCast_ne_coe_top (since := "2024-10-22")]

theorem ENat.nat_ne_coe_top (n : ℕ) :

↑n ≠ ↑⊤

Alias of ENat.natCast_ne_coe_top.

theorem ENat.one_le_iff_ne_zero_withTop {n : WithTop ℕ∞} :

1 ≤ n ↔ n ≠ 0

theorem ENat.natCast_le_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : ↑⊤ ≤ N) (n : ℕ) :

↑n ≤ N

theorem ENat.natCast_lt_of_coe_top_le_withTop {N : WithTop ℕ∞} (hN : ↑⊤ ≤ N) (n : ℕ) :

↑n < N

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

Specialization of WithTop.map to ENat.

Equations

ENat.map f k = WithTop.map f k

@[simp]

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

map f ⊤ = ⊤

@[simp]

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

map f ↑a = ↑(f a)

@[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_natCast_nonneg {n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] :

0 ≤ map Nat.cast n

theorem ENat.map_natCast_strictMono {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :

StrictMono (map Nat.cast)

theorem ENat.map_natCast_injective {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :

Function.Injective (map Nat.cast)

@[simp]

theorem ENat.map_natCast_inj {m n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :

map Nat.cast m = map Nat.cast n ↔ m = n

@[simp]

theorem ENat.map_natCast_eq_zero {n : ℕ∞} {α : Type u_1} [AddMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] :

map Nat.cast n = 0 ↔ n = 0

@[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' := ⋯ }

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' := ⋯ }

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' := ⋯ }

@[simp]

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

⇑f.ENatMap = ENat.map ⇑f

def AddMonoidHom.ENatMap {N : Type u_2} [AddZeroClass N] (f : ℕ →+ N) :

ℕ∞ →+ WithTop N

A version of WithTop.map for AddMonoidHoms.

Equations

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

@[simp]

theorem AddMonoidHom.ENatMap_apply {N : Type u_2} [AddZeroClass N] (f : ℕ →+ N) :

⇑f.ENatMap = ENat.map ⇑f

def MonoidWithZeroHom.ENatMap {S : Type u_2} [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : ℕ →*₀ S) (hf : Function.Injective ⇑f) :

ℕ∞ →*₀ WithTop S

A version of ENat.map for MonoidWithZeroHoms.

Equations

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

@[simp]

theorem MonoidWithZeroHom.ENatMap_apply {S : Type u_2} [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : ℕ →*₀ S) (hf : Function.Injective ⇑f) :

⇑(f.ENatMap hf) = ENat.map ⇑f

def RingHom.ENatMap {S : Type u_2} [CommSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective ⇑f) :

ℕ∞ →+* WithTop S

A version of ENat.map for RingHoms.

Equations

f.ENatMap hf = { toFun := (↑(f.toMonoidWithZeroHom.ENatMap hf)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.ENatMap_apply {S : Type u_2} [CommSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective ⇑f) :

⇑(f.ENatMap hf) = (↑(f.toMonoidWithZeroHom.ENatMap hf)).toFun

theorem WithBot.lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} :

n < ↑m + 1 ↔ n ≤ ↑m

theorem WithBot.add_one_le_iff {n : ℕ} {m : WithBot ℕ∞} :

↑n + 1 ≤ m ↔ ↑n < m