mathlib documentation

data.nat.enat

Natural numbers with infinity

The natural numbers and an extra top element ⊤.

Main definitions

The following instances are defined:

There is no additive analogue of monoid_with_zero; if there were then enat could be an add_monoid_with_top.

to_with_top : the map from enat to with_top ℕ, with theorems that it plays well with + and ≤.
with_top_add_equiv : enat ≃+ with_top ℕ
with_top_order_iso : enat ≃o with_top ℕ

Implementation details

enat is defined to be roption ℕ.

+ and ≤ are defined on enat, but there is an issue with * because it's not clear what 0 * ⊤ should be. mul is hence left undefined. Similarly ⊤ - ⊤ is ambiguous so there is no - defined on enat.

Before the open_locale classical line, various proofs are made with decidability assumptions. This can cause issues -- see for example the non-simp lemma to_with_top_zero proved by rfl, followed by @[simp] lemma to_with_top_zero' whose proof uses convert.

Tags

enat, with_top ℕ

def enat :

Type

Type of natural numbers with infinity

Equations

enat = roption ℕ

@[instance]

def enat.has_zero :

Equations

enat.has_zero = {zero := roption.some 0}

@[instance]

def enat.inhabited :

Equations

enat.inhabited = {default := 0}

@[instance]

def enat.has_one :

Equations

enat.has_one = {one := roption.some 1}

@[instance]

def enat.has_add :

Equations

enat.has_add = {add := λ (x y : enat), {dom := x.dom ∧ y.dom, get := λ (h : x.dom ∧ y.dom), x.get _ + y.get _}}

@[instance]

def enat.has_coe :

has_coe ℕ enat

Equations

enat.has_coe = {coe := roption.some ℕ}

@[instance]

def enat.decidable (n : ℕ) :

decidable ↑n.dom

Equations

enat.decidable n = is_true trivial

@[simp]

theorem enat.coe_inj {x y : ℕ} :

↑x = ↑y ↔ x = y

@[instance]

def enat.add_comm_monoid :

add_comm_monoid enat

Equations

enat.add_comm_monoid = {add := has_add.add enat.has_add, add_assoc := enat.add_comm_monoid._proof_1, zero := 0, zero_add := enat.add_comm_monoid._proof_2, add_zero := enat.add_comm_monoid._proof_3, add_comm := enat.add_comm_monoid._proof_4}

@[instance]

def enat.has_le :

Equations

enat.has_le = {le := λ (x y : enat), ∃ (h : y.dom → x.dom), ∀ (hy : y.dom), x.get _ ≤ y.get hy}

@[instance]

def enat.has_top :

Equations

enat.has_top = {top := roption.none ℕ}

@[instance]

def enat.has_bot :

Equations

enat.has_bot = {bot := 0}

@[instance]

def enat.has_sup :

Equations

enat.has_sup = {sup := λ (x y : enat), {dom := x.dom ∧ y.dom, get := λ (h : x.dom ∧ y.dom), x.get _ ⊔ y.get _}}

theorem enat.cases_on {P : enat → Prop} (a : enat) (a_1 : P ⊤) (a_2 : ∀ (n : ℕ), P ↑n) :

P a

@[simp]

theorem enat.top_add (x : enat) :

@[simp]

theorem enat.add_top (x : enat) :

@[simp]

theorem enat.coe_zero :

↑0 = 0

@[simp]

theorem enat.coe_one :

↑1 = 1

@[simp]

theorem enat.coe_add (x y : ℕ) :

↑(x + y) = ↑x + ↑y

@[simp]

theorem enat.get_coe {x : ℕ} :

↑x.get true.intro = x

theorem enat.coe_add_get {x : ℕ} {y : enat} (h : (↑x + y).dom) :

(↑x + y).get h = x + y.get _

@[simp]

theorem enat.get_add {x y : enat} (h : (x + y).dom) :

(x + y).get h = x.get _ + y.get _

@[simp]

theorem enat.coe_get {x : enat} (h : x.dom) :

↑(x.get h) = x

@[simp]

theorem enat.get_zero (h : 0.dom) :

0.get h = 0

@[simp]

theorem enat.get_one (h : 1.dom) :

1.get h = 1

theorem enat.dom_of_le_some {x : enat} {y : ℕ} (a : x ≤ ↑y) :

@[instance]

def enat.partial_order :

partial_order enat

Equations

enat.partial_order = {le := has_le.le enat.has_le, lt := preorder.lt._default has_le.le, le_refl := enat.partial_order._proof_1, le_trans := enat.partial_order._proof_2, lt_iff_le_not_le := enat.partial_order._proof_3, le_antisymm := enat.partial_order._proof_4}

@[simp]

theorem enat.coe_le_coe {x y : ℕ} :

↑x ≤ ↑y ↔ x ≤ y

@[simp]

theorem enat.coe_lt_coe {x y : ℕ} :

↑x < ↑y ↔ x < y

theorem enat.get_le_get {x y : enat} {hx : x.dom} {hy : y.dom} :

x.get hx ≤ y.get hy ↔ x ≤ y

@[instance]

def enat.semilattice_sup_bot :

semilattice_sup_bot enat

Equations

enat.semilattice_sup_bot = {bot := ⊥, le := partial_order.le enat.partial_order, lt := partial_order.lt enat.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := enat.semilattice_sup_bot._proof_1, sup := has_sup.sup enat.has_sup, le_sup_left := enat.semilattice_sup_bot._proof_2, le_sup_right := enat.semilattice_sup_bot._proof_3, sup_le := enat.semilattice_sup_bot._proof_4}

@[instance]

def enat.order_top :

Equations

enat.order_top = {top := ⊤, le := semilattice_sup_bot.le enat.semilattice_sup_bot, lt := semilattice_sup_bot.lt enat.semilattice_sup_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_top := enat.order_top._proof_1}

theorem enat.top_eq_none :

⊤ = roption.none

theorem enat.coe_lt_top (x : ℕ) :

@[simp]

theorem enat.coe_ne_top (x : ℕ) :

theorem enat.ne_top_iff {x : enat} :

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

theorem enat.ne_top_iff_dom {x : enat} :

x ≠ ⊤ ↔ x.dom

theorem enat.ne_top_of_lt {x y : enat} (h : x < y) :

theorem enat.pos_iff_one_le {x : enat} :

0 < x ↔ 1 ≤ x

@[instance]

def enat.decidable_linear_order :

decidable_linear_order enat

Equations

enat.decidable_linear_order = {le := partial_order.le enat.partial_order, lt := partial_order.lt enat.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := enat.decidable_linear_order._proof_1, decidable_le := classical.dec_rel has_le.le, decidable_eq := decidable_eq_of_decidable_le (classical.dec_rel has_le.le), decidable_lt := decidable_lt_of_decidable_le (classical.dec_rel has_le.le)}

@[instance]

def enat.bounded_lattice :

bounded_lattice enat

Equations

enat.bounded_lattice = {sup := semilattice_sup_bot.sup enat.semilattice_sup_bot, le := order_top.le enat.order_top, lt := order_top.lt enat.order_top, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := min enat.decidable_linear_order, inf_le_left := _, inf_le_right := _, le_inf := enat.bounded_lattice._proof_1, top := order_top.top enat.order_top, le_top := _, bot := semilattice_sup_bot.bot enat.semilattice_sup_bot, bot_le := _}

theorem enat.sup_eq_max {a b : enat} :

a ⊔ b = max a b

theorem enat.inf_eq_min {a b : enat} :

a ⊓ b = min a b

@[instance]

def enat.ordered_add_comm_monoid :

ordered_add_comm_monoid enat

Equations

enat.ordered_add_comm_monoid = {add := add_comm_monoid.add enat.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero enat.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := decidable_linear_order.le enat.decidable_linear_order, lt := decidable_linear_order.lt enat.decidable_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := enat.ordered_add_comm_monoid._proof_1, lt_of_add_lt_add_left := enat.ordered_add_comm_monoid._proof_2}

@[instance]

def enat.canonically_ordered_add_monoid :

canonically_ordered_add_monoid enat

Equations

enat.canonically_ordered_add_monoid = {add := ordered_add_comm_monoid.add enat.ordered_add_comm_monoid, add_assoc := _, zero := ordered_add_comm_monoid.zero enat.ordered_add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, le := semilattice_sup_bot.le enat.semilattice_sup_bot, lt := semilattice_sup_bot.lt enat.semilattice_sup_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, lt_of_add_lt_add_left := _, bot := semilattice_sup_bot.bot enat.semilattice_sup_bot, bot_le := _, le_iff_exists_add := enat.canonically_ordered_add_monoid._proof_1}

theorem enat.add_lt_add_right {x y z : enat} (h : x < y) (hz : z ≠ ⊤) :

x + z < y + z

theorem enat.add_lt_add_iff_right {x y z : enat} (hz : z ≠ ⊤) :

x + z < y + z ↔ x < y

theorem enat.add_lt_add_iff_left {x y z : enat} (hz : z ≠ ⊤) :

z + x < z + y ↔ x < y

theorem enat.lt_add_iff_pos_right {x y : enat} (hx : x ≠ ⊤) :

x < x + y ↔ 0 < y

theorem enat.lt_add_one {x : enat} (hx : x ≠ ⊤) :

x < x + 1

theorem enat.le_of_lt_add_one {x y : enat} (h : x < y + 1) :

x ≤ y

theorem enat.add_one_le_of_lt {x y : enat} (h : x < y) :

x + 1 ≤ y

theorem enat.add_one_le_iff_lt {x y : enat} (hx : x ≠ ⊤) :

x + 1 ≤ y ↔ x < y

theorem enat.lt_add_one_iff_lt {x y : enat} (hx : x ≠ ⊤) :

x < y + 1 ↔ x ≤ y

theorem enat.add_eq_top_iff {a b : enat} :

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

theorem enat.add_right_cancel_iff {a b c : enat} (hc : c ≠ ⊤) :

a + c = b + c ↔ a = b

theorem enat.add_left_cancel_iff {a b c : enat} (ha : a ≠ ⊤) :

a + b = a + c ↔ b = c

def enat.to_with_top (x : enat) [decidable x.dom] :

Computably converts an enat to a with_top ℕ.

Equations

x.to_with_top = roption.to_option x

theorem enat.to_with_top_top :

⊤.to_with_top = ⊤

@[simp]

theorem enat.to_with_top_top' {h : decidable ⊤.dom} :

⊤.to_with_top = ⊤

theorem enat.to_with_top_zero :

0.to_with_top = 0

@[simp]

theorem enat.to_with_top_zero' {h : decidable 0.dom} :

0.to_with_top = 0

theorem enat.to_with_top_coe (n : ℕ) :

↑n.to_with_top = ↑n

@[simp]

theorem enat.to_with_top_coe' (n : ℕ) {h : decidable ↑n.dom} :

↑n.to_with_top = ↑n

@[simp]

theorem enat.to_with_top_le {x y : enat} [decidable x.dom] [decidable y.dom] :

x.to_with_top ≤ y.to_with_top ↔ x ≤ y

@[simp]

theorem enat.to_with_top_lt {x y : enat} [decidable x.dom] [decidable y.dom] :

x.to_with_top < y.to_with_top ↔ x < y

@[simp]

theorem enat.to_with_top_add {x y : enat} :

(x + y).to_with_top = x.to_with_top + y.to_with_top

def enat.with_top_equiv :

enat ≃ with_top ℕ

equiv between enat and with_top ℕ (for the order isomorphism see with_top_order_iso).

Equations

enat.with_top_equiv = {to_fun := λ (x : enat), x.to_with_top, inv_fun := λ (x : with_top ℕ), enat.with_top_equiv._match_1 x, left_inv := enat.with_top_equiv._proof_1, right_inv := enat.with_top_equiv._proof_2}
enat.with_top_equiv._match_1 (some n) = ↑n
enat.with_top_equiv._match_1 none = ⊤

@[simp]

theorem enat.with_top_equiv_top :

⇑enat.with_top_equiv ⊤ = ⊤

@[simp]

theorem enat.with_top_equiv_coe (n : ℕ) :

⇑enat.with_top_equiv ↑n = ↑n

@[simp]

theorem enat.with_top_equiv_zero :

⇑enat.with_top_equiv 0 = 0

@[simp]

theorem enat.with_top_equiv_le {x y : enat} :

⇑enat.with_top_equiv x ≤ ⇑enat.with_top_equiv y ↔ x ≤ y

@[simp]

theorem enat.with_top_equiv_lt {x y : enat} :

⇑enat.with_top_equiv x < ⇑enat.with_top_equiv y ↔ x < y

def enat.with_top_order_iso :

enat ≃o with_top ℕ

to_with_top induces an order isomorphism between enat and with_top ℕ.

Equations

enat.with_top_order_iso = {to_equiv := {to_fun := enat.with_top_equiv.to_fun, inv_fun := enat.with_top_equiv.inv_fun, left_inv := enat.with_top_order_iso._proof_1, right_inv := enat.with_top_order_iso._proof_2}, map_rel_iff' := enat.with_top_order_iso._proof_3}

@[simp]

theorem enat.with_top_equiv_symm_top :

⇑(enat.with_top_equiv.symm) ⊤ = ⊤

@[simp]

theorem enat.with_top_equiv_symm_coe (n : ℕ) :

⇑(enat.with_top_equiv.symm) ↑n = ↑n

@[simp]

theorem enat.with_top_equiv_symm_zero :

⇑(enat.with_top_equiv.symm) 0 = 0

@[simp]

theorem enat.with_top_equiv_symm_le {x y : with_top ℕ} :

⇑(enat.with_top_equiv.symm) x ≤ ⇑(enat.with_top_equiv.symm) y ↔ x ≤ y

@[simp]

theorem enat.with_top_equiv_symm_lt {x y : with_top ℕ} :

⇑(enat.with_top_equiv.symm) x < ⇑(enat.with_top_equiv.symm) y ↔ x < y

def enat.with_top_add_equiv :

enat ≃+ with_top ℕ

to_with_top induces an additive monoid isomorphism between enat and with_top ℕ.

Equations

enat.with_top_add_equiv = {to_fun := enat.with_top_equiv.to_fun, inv_fun := enat.with_top_equiv.inv_fun, left_inv := enat.with_top_add_equiv._proof_1, right_inv := enat.with_top_add_equiv._proof_2, map_add' := enat.with_top_add_equiv._proof_3}

theorem enat.lt_wf :

well_founded has_lt.lt

@[instance]

def enat.has_well_founded :

has_well_founded enat

Equations

enat.has_well_founded = {r := has_lt.lt (preorder.to_has_lt enat), wf := enat.lt_wf}