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 : Zero ℕ∞

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 : Bot ℕ∞

Equations

• instENatBot = WithTop.instBot

instance instENatSub : Sub ℕ∞

Equations

• instENatSub = WithTop.instSub

instance instENatLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop ℕ∞

Equations

• instENatLinearOrderedAddCommMonoidWithTop = WithTop.linearOrderedAddCommMonoidWithTop

instance instENatWellFoundedRelation : WellFoundedRelation ℕ∞

Equations

• instENatWellFoundedRelation = sizeOfWFRel

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) : m * ⊤ = ⊤

@[simp]

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

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

@[simp]

theorem ENat.top_pow {n : ℕ} (hn : n ≠ 0) : ⊤ ^ n = ⊤

@[simp]

theorem ENat.pow_eq_top_iff {a : ℕ∞} {n : ℕ} : a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0

theorem ENat.pow_ne_top_iff {a : ℕ∞} {n : ℕ} : a ^ n ≠ ⊤ ↔ a ≠ ⊤ ∨ n = 0

@[simp]

theorem ENat.pow_lt_top_iff {a : ℕ∞} {n : ℕ} : a ^ n < ⊤ ↔ a < ⊤ ∨ n = 0

theorem ENat.eq_top_of_pow {a : ℕ∞} (n : ℕ) (ha : a ^ n = ⊤) : a = ⊤

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_1 }

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_1, map_one' := ENat.toNatHom._proof_2, 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 : toNat 0 = 0

@[simp]

theorem ENat.toNat_one : toNat 1 = 1

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

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

@[simp]

theorem ENat.top_ne_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ ≠ OfNat.ofNat a

@[simp]

theorem ENat.top_ne_zero : ⊤ ≠ 0

@[simp]

theorem ENat.top_ne_one : ⊤ ≠ 1

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

@[simp]

theorem ENat.one_ne_top : 1 ≠ ⊤

@[simp]

theorem ENat.top_sub_coe (a : ℕ) : ⊤ - ↑a = ⊤

@[simp]

theorem ENat.top_sub_one : ⊤ - 1 = ⊤

@[simp]

theorem ENat.top_sub_ofNat (a : ℕ) [a.AtLeastTwo] : ⊤ - OfNat.ofNat a = ⊤

@[simp]

theorem ENat.top_pos : 0 < ⊤

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

theorem ENat.zero_lt_top : 0 < ⊤

Alias of ENat.top_pos.

@[simp]

theorem ENat.one_lt_top : 1 < ⊤

@[simp]

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

@[simp]

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) : 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_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.lt_coe_add_one_iff {m : ℕ∞} {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

Version of WithTop.forall_coe_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_coe_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_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 : ℕ∞) : WithTop α

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

instance ENat.instNoZeroDivisors : NoZeroDivisors ℕ∞

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