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

IsOrderedRing ℕ∞

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

Equations

instSubENat = { sub := instSubENat._aux_1 }

@[instance_reducible]

instance instLinearOrderENat :

LinearOrder ℕ∞

Equations

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

@[instance_reducible]

instance instLTENat :

Equations

instLTENat = { lt := instLTENat._aux_1 }

@[instance_reducible]

instance instSuccOrderENat :

SuccOrder ℕ∞

Equations

instSuccOrderENat = { succ := instSuccOrderENat._aux_1, le_succ := instSuccOrderENat._proof_3, max_of_succ_le := @instSuccOrderENat._proof_4, succ_le_of_lt := @instSuccOrderENat._proof_5 }

@[instance_reducible]

instance instCommSemiringENat :

CommSemiring ℕ∞

Equations

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

instance instZeroLEOneClassENat :

ZeroLEOneClass ℕ∞

instance instCanonicallyOrderedAddENat :

CanonicallyOrderedAdd ℕ∞

instance instOrderedSubENat :

OrderedSub ℕ∞

@[instance_reducible]

instance instLinearOrderedAddCommMonoidWithTopENat :

LinearOrderedAddCommMonoidWithTop ℕ∞

Equations

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

instance instCharZeroENat :

CharZero ℕ∞

@[instance_reducible]

instance instOrderTopENat :

OrderTop ℕ∞

Equations

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

@[instance_reducible]

instance instAddMonoidWithOneENat :

AddMonoidWithOne ℕ∞

Equations

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

instance instWellFoundedLTENat :

WellFoundedLT ℕ∞

instance instNontrivialENat :

Nontrivial ℕ∞

instance instNoZeroDivisorsENat :

NoZeroDivisors ℕ∞

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

@[simp]

theorem ENat.succ_natCast (n : ℕ) :

SuccOrder.succ ↑n = ↑(n + 1)

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

theorem ENat.succ_coe (n : ℕ) :

SuccOrder.succ ↑n = ↑(n + 1)

Alias of ENat.succ_natCast.

@[simp]

theorem ENat.succ_top :

SuccOrder.succ ⊤ = ⊤

@[instance_reducible]

instance ENat.instSuccAddOrder :

SuccAddOrder ℕ∞

Equations

ENat.instSuccAddOrder = { toSuccOrder := instSuccOrderENat, succ_eq_add_one := ⋯ }

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_mul (m n : ℕ) :

↑(m * n) = ↑m * ↑n

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

theorem ENat.coe_mul (m n : ℕ) :

↑(m * n) = ↑m * ↑n

Alias of ENat.natCast_mul.

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

@[simp]

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

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

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

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

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

Instances For

@[simp]

theorem ENat.coe_toNatHom :

⇑toNatHom = toNat

theorem ENat.toNatHom_apply (n : ℕ) :

toNatHom ↑n = (↑n).toNat

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

@[simp]

theorem ENat.natCast_toNat_eq_self {n : ℕ∞} :

↑n.toNat = n ↔ n ≠ ⊤

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

theorem ENat.coe_toNat_eq_self {n : ℕ∞} :

↑n.toNat = n ↔ n ≠ ⊤

Alias of ENat.natCast_toNat_eq_self.

theorem ENat.natCast_toNat {n : ℕ∞} :

n ≠ ⊤ → ↑n.toNat = n

Alias of the reverse direction of ENat.natCast_toNat_eq_self.

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

theorem ENat.coe_toNat {n : ℕ∞} :

n ≠ ⊤ → ↑n.toNat = n

Alias of ENat.natCast_toNat.

Alias of the reverse direction of ENat.natCast_toNat_eq_self.

@[simp]

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

n.toNat = m ↔ n = ↑m

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

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

n.toNat = m ↔ n = ↑m

Alias of ENat.toNat_eq_iff_eq_natCast.

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

@[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_natCast {m : ℕ∞} {n : ℕ} (h : m ≤ ↑n) :

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

theorem ENat.toNat_le_of_le_coe {m : ℕ∞} {n : ℕ} (h : m ≤ ↑n) :

Alias of ENat.toNat_le_of_le_natCast.

theorem ENat.toNat_le_toNat {m n : ℕ∞} (h : m ≤ n) (hn : n ≠ ⊤) :

m.toNat ≤ n.toNat

@[deprecated Order.succ_eq_add_one (since := "2026-05-25")]

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.add_one_le_iff' {m n : ℕ∞} (hn : n ≠ ⊤) :

m + 1 ≤ n ↔ m < n

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

↑m + 1 ≤ n ↔ ↑m < n

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

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

↑m + 1 ≤ n ↔ ↑m < n

Alias of ENat.natCast_add_one_le_iff.

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

m + 1 ≤ ↑n ↔ m < ↑n

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

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

m + 1 ≤ ↑n ↔ m < ↑n

Alias of ENat.add_one_le_natCast_iff.

@[deprecated Order.one_le_iff_ne_zero (since := "2026-05-25")]

theorem ENat.one_le_iff_ne_zero {n : ℕ∞} :

1 ≤ n ↔ n ≠ 0

@[deprecated Order.lt_one_iff (since := "2026-05-25")]

theorem ENat.lt_one_iff_eq_zero {n : ℕ∞} :

n < 1 ↔ n = 0

@[deprecated Order.le_one_iff (since := "2026-05-25")]

theorem ENat.le_one_iff_eq_zero_or_eq_one {n : ℕ∞} :

n ≤ 1 ↔ n = 0 ∨ n = 1

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

m < n + 1 ↔ m ≤ n

theorem ENat.lt_add_one_iff' {m n : ℕ∞} (hm : m ≠ ⊤) :

m < n + 1 ↔ m ≤ n

@[simp]

theorem ENat.lt_two_iff {n : ℕ∞} :

n < 2 ↔ n ≤ 1

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

m < ↑n + 1 ↔ m ≤ ↑n

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

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

m < ↑n + 1 ↔ m ≤ ↑n

Alias of ENat.lt_natCast_add_one_iff.

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

↑m < n + 1 ↔ ↑m ≤ n

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

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

↑m < n + 1 ↔ ↑m ≤ n

Alias of ENat.natCast_lt_add_one_iff.

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.

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

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

@[deprecated add_pos_of_right (since := "2026-05-25")]

theorem ENat.add_one_pos {n : ℕ∞} :

0 < n + 1

theorem ENat.natCast_lt_succ {n : ℕ} :

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

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

a + b ≤ c → b ≤ c - a

theorem ENat.le_sub_of_add_le_right {a b c : ℕ∞} (hb : b ≠ ⊤) :

a + b ≤ c → a ≤ c - b

theorem ENat.le_sub_one_of_lt {a b : ℕ∞} (h : a < b) :

a ≤ b - 1

theorem ENat.lt_add_left {n k : ℕ∞} (h : n ≠ ⊤) (h' : 0 < k) :

n < k + n

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_right_strictMono {a : ℕ∞} (ha : a ≠ 0) (h_top : a ≠ ⊤) :

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

theorem ENat.mul_left_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

@[instance_reducible]

instance ENat.instUniqueUnits :

Unique ℕ∞ˣ

Equations

ENat.instUniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }

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 ≠ ↑⊤

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

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

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

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

Instances For

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

Instances For

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

Instances For

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

@[simp]

theorem ENat.map_natCast_mul {R : Type u_2} [NonAssocSemiring R] [DecidableEq R] [CharZero R] (a b : ℕ∞) :

map Nat.cast (a * b) = map Nat.cast a * map Nat.cast b

@[simp]

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

↑↑n = ↑n

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

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

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

n < ↑m + 1 ↔ n ≤ ↑m

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

↑n + 1 ≤ m ↔ ↑n < m

theorem ENat.WithBot.add_one_le_natCast_iff {n : WithBot ℕ∞} {m : ℕ} :

n + 1 ≤ ↑m ↔ n < ↑m

@[simp]

theorem ENat.WithBot.add_one_le_zero_iff (n : WithBot ℕ∞) :

n + 1 ≤ 0 ↔ n = ⊥

@[simp]

theorem ENat.WithBot.add_natCast_cancel {a b : WithBot ℕ∞} {c : ℕ} :

a + ↑c = b + ↑c ↔ a = b

@[simp]

theorem ENat.WithBot.add_one_cancel {a b : WithBot ℕ∞} :

a + 1 = b + 1 ↔ a = b

theorem ENat.WithBot.add_ofNat_cancel {a b : WithBot ℕ∞} {c : ℕ} [c.AtLeastTwo] :

a + OfNat.ofNat c = b + OfNat.ofNat c ↔ a = b

@[simp]

theorem ENat.WithBot.natCast_add_cancel {a b : WithBot ℕ∞} {c : ℕ} :

↑c + a = ↑c + b ↔ a = b

@[simp]

theorem ENat.WithBot.one_add_cancel {a b : WithBot ℕ∞} :

1 + a = 1 + b ↔ a = b

theorem ENat.WithBot.ofNat_add_cancel {a b : WithBot ℕ∞} {c : ℕ} [c.AtLeastTwo] :

OfNat.ofNat c + a = OfNat.ofNat c + b ↔ a = b

theorem ENat.WithBot.add_le_add_natCast_right_iff {a b : WithBot ℕ∞} {c : ℕ} :

a + ↑c ≤ b + ↑c ↔ a ≤ b

theorem ENat.WithBot.add_le_add_one_right_iff {a b : WithBot ℕ∞} :

a + 1 ≤ b + 1 ↔ a ≤ b

theorem ENat.WithBot.add_le_add_natCast_left_iff {a b : WithBot ℕ∞} {c : ℕ} :

↑c + a ≤ ↑c + b ↔ a ≤ b

theorem ENat.WithBot.add_le_add_one_left_iff {a b : WithBot ℕ∞} :

1 + a ≤ 1 + b ↔ a ≤ b