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.
Extended natural numbers ℕ∞ = WithTop ℕ∞ = WithTop ℕ
.
Equations
- «termℕ∞» = Lean.ParserDescr.node `termℕ∞ 1024 (Lean.ParserDescr.symbol "ℕ∞")
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
instance
ENat.instIsWellOrderENatLtToLTToPreorderToPartialOrderToOrderedSemiringToOrderedCommSemiringInstENatCanonicallyOrderedCommSemiring :
IsWellOrder ℕ∞ fun x x_1 => x < x_1
Equations
- One or more equations did not get rendered due to their size.
Equations
- ENat.canLift = WithTop.canLift
Conversion of ℕ∞∞
to ℕ
sending ∞∞
to 0
.
Equations
- ENat.toNat = { toZeroHom := { toFun := WithTop.untop' 0, map_zero' := ENat.toNat.proof_1 }, map_one' := ENat.toNat.proof_2, map_mul' := ENat.toNat.proof_3 }
@[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
Alias of the reverse direction of ENat.coe_toNat_eq_self
.
theorem
ENat.toNat_add
{m : ℕ∞}
{n : ℕ∞}
(hm : m ≠ ⊤)
(hn : n ≠ ⊤)
:
↑ENat.toNat (m + n) = ↑ENat.toNat m + ↑ENat.toNat n
theorem
ENat.toNat_sub
{n : ℕ∞}
(hn : n ≠ ⊤)
(m : ℕ∞)
:
↑ENat.toNat (m - n) = ↑ENat.toNat m - ↑ENat.toNat n