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

+ 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 = part ℕ

def enat.some :

The computable embedding ℕ → enat.

This coincides with the coercion coe : ℕ → enat, see enat.some_eq_coe. However, coe is noncomputable so some is preferable when computability is a concern.

Equations

enat.some = part.some

@[protected, instance]

def enat.has_zero :

Equations

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

@[protected, instance]

def enat.inhabited :

Equations

enat.inhabited = {default := 0}

@[protected, instance]

def enat.has_one :

Equations

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

@[protected, 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 _}}

@[protected, instance]

def enat.dom.decidable (n : ℕ) :

decidable (enat.some n).dom

Equations

enat.dom.decidable n = is_true trivial

theorem enat.some_eq_coe (n : ℕ) :

enat.some n = ↑n

@[simp]

theorem enat.coe_inj {x y : ℕ} :

↑x = ↑y ↔ x = y

@[simp]

theorem enat.dom_some (x : ℕ) :

(enat.some x).dom

@[simp]

theorem enat.dom_coe (x : ℕ) :

@[protected, 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, nsmul := add_monoid.nsmul._default 0 has_add.add enat.add_comm_monoid._proof_4 enat.add_comm_monoid._proof_5, nsmul_zero' := enat.add_comm_monoid._proof_6, nsmul_succ' := enat.add_comm_monoid._proof_7, add_comm := enat.add_comm_monoid._proof_8}

@[protected, 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}

@[protected, instance]

def enat.has_top :

Equations

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

@[protected, instance]

def enat.has_bot :

Equations

enat.has_bot = {bot := 0}

@[protected, 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.le_def (x y : enat) :

x ≤ y ↔ ∃ (h : y.dom → x.dom), ∀ (hy : y.dom), x.get _ ≤ y.get hy

@[protected]

theorem enat.cases_on' {P : enat → Prop} (a : enat) :

P ⊤ → (∀ (n : ℕ), P (enat.some n)) → P a

@[protected]

theorem enat.cases_on {P : enat → Prop} (a : enat) :

P ⊤ → (∀ (n : ℕ), P ↑n) → P a

@[simp]

theorem enat.top_add (x : enat) :

@[simp]

theorem enat.add_top (x : enat) :

@[simp]

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

↑(x.get h) = x

@[simp, norm_cast]

theorem enat.get_coe' (x : ℕ) (h : ↑x.dom) :

↑x.get h = x

theorem enat.get_coe {x : ℕ} :

↑x.get _ = 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.get_zero (h : 0.dom) :

0.get h = 0

@[simp]

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

1.get h = 1

theorem enat.get_eq_iff_eq_some {a : enat} {ha : a.dom} {b : ℕ} :

a.get ha = b ↔ a = enat.some b

theorem enat.get_eq_iff_eq_coe {a : enat} {ha : a.dom} {b : ℕ} :

a.get ha = b ↔ a = ↑b

theorem enat.dom_of_le_of_dom {x y : enat} :

x ≤ y → y.dom → x.dom

theorem enat.dom_of_le_some {x : enat} {y : ℕ} (h : x ≤ enat.some y) :

theorem enat.dom_of_le_coe {x : enat} {y : ℕ} (h : x ≤ ↑y) :

@[protected, instance]

def enat.decidable_le (x y : enat) [decidable x.dom] [decidable y.dom] :

decidable (x ≤ y)

Equations

x.decidable_le y = dite x.dom (λ (hx : x.dom), decidable_of_decidable_of_iff (show decidable (∀ (hy : y.dom), x.get hx ≤ y.get hy), from forall_prop_decidable (λ (hy : y.dom), x.get hx ≤ y.get hy)) _) (λ (hx : ¬x.dom), dite y.dom (λ (hy : y.dom), is_false _) (λ (hy : ¬y.dom), is_true _))

def enat.coe_hom :

The coercion ℕ → enat preserves 0 and addition.

Equations

enat.coe_hom = {to_fun := coe coe_to_lift, map_zero' := _, map_add' := enat.coe_hom._proof_1}

@[simp]

theorem enat.coe_coe_hom :

⇑enat.coe_hom = coe

@[protected, 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}

theorem enat.lt_def (x y : enat) :

x < y ↔ ∃ (hx : x.dom), ∀ (hy : y.dom), x.get hx < y.get hy

@[simp, norm_cast]

theorem enat.coe_le_coe {x y : ℕ} :

↑x ≤ ↑y ↔ x ≤ y

@[simp, norm_cast]

theorem enat.coe_lt_coe {x y : ℕ} :

↑x < ↑y ↔ x < y

@[simp]

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

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

theorem enat.le_coe_iff (x : enat) (n : ℕ) :

x ≤ ↑n ↔ ∃ (h : x.dom), x.get h ≤ n

theorem enat.lt_coe_iff (x : enat) (n : ℕ) :

x < ↑n ↔ ∃ (h : x.dom), x.get h < n

theorem enat.coe_le_iff (n : ℕ) (x : enat) :

↑n ≤ x ↔ ∀ (h : x.dom), n ≤ x.get h

theorem enat.coe_lt_iff (n : ℕ) (x : enat) :

↑n < x ↔ ∀ (h : x.dom), n < x.get h

@[protected]

theorem enat.zero_lt_one :

0 < 1

@[protected, instance]

def enat.semilattice_sup :

semilattice_sup enat

Equations

enat.semilattice_sup = {sup := has_sup.sup enat.has_sup, 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_sup_left := enat.semilattice_sup._proof_1, le_sup_right := enat.semilattice_sup._proof_2, sup_le := enat.semilattice_sup._proof_3}

@[protected, instance]

def enat.order_bot :

Equations

enat.order_bot = {bot := ⊥, bot_le := enat.order_bot._proof_1}

@[protected, instance]

def enat.order_top :

Equations

enat.order_top = {top := ⊤, le_top := enat.order_top._proof_1}

theorem enat.dom_of_lt {x y : enat} :

x < y → x.dom

theorem enat.top_eq_none :

⊤ = part.none

@[simp]

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.eq_top_iff_forall_lt (x : enat) :

x = ⊤ ↔ ∀ (n : ℕ), ↑n < x

theorem enat.eq_top_iff_forall_le (x : enat) :

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

theorem enat.pos_iff_one_le {x : enat} :

0 < x ↔ 1 ≤ x

@[protected, instance]

def enat.has_le.le.is_total :

is_total enat has_le.le

@[protected, instance]

noncomputable def enat.linear_order :

linear_order enat

Equations

enat.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.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), max := has_sup.sup enat.has_sup, max_def := enat.linear_order._proof_2, min := min_default (λ (a b : enat), classical.dec_rel has_le.le a b), min_def := enat.linear_order._proof_3}

@[protected, instance]

def enat.bounded_order :

bounded_order enat

Equations

enat.bounded_order = {top := order_top.top enat.order_top, le_top := _, bot := order_bot.bot enat.order_bot, bot_le := _}

@[protected, instance]

noncomputable def enat.lattice :

Equations

enat.lattice = {sup := semilattice_sup.sup enat.semilattice_sup, le := semilattice_sup.le enat.semilattice_sup, lt := semilattice_sup.lt enat.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := min enat.linear_order, inf_le_left := _, inf_le_right := _, le_inf := enat.lattice._proof_1}

@[protected, 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 := _, nsmul := add_comm_monoid.nsmul enat.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := linear_order.le enat.linear_order, lt := linear_order.lt enat.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := enat.ordered_add_comm_monoid._proof_1}

@[protected, 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 := _, nsmul := ordered_add_comm_monoid.nsmul enat.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := semilattice_sup.le enat.semilattice_sup, lt := semilattice_sup.lt enat.semilattice_sup, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, bot := order_bot.bot enat.order_bot, bot_le := _, le_iff_exists_add := enat.canonically_ordered_add_monoid._proof_1}

@[protected]

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

x + z < y + z

@[protected]

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

x + z < y + z ↔ x < y

@[protected]

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

z + x < z + y ↔ x < y

@[protected]

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

@[protected]

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

a + c = b + c ↔ a = b

@[protected]

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 = part.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_some (n : ℕ) :

(enat.some n).to_with_top = ↑n

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

↑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

noncomputable 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

noncomputable 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

noncomputable 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

@[protected, 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}

def enat.find (P : ℕ → Prop) [decidable_pred P] :

The smallest enat satisfying a (decidable) predicate P : ℕ → Prop

Equations

enat.find P = {dom := ∃ (n : ℕ), P n, get := nat.find (λ (a : ℕ), _inst_1 a)}

@[simp]

theorem enat.find_get (P : ℕ → Prop) [decidable_pred P] (h : (enat.find P).dom) :

(enat.find P).get h = nat.find h

theorem enat.find_dom (P : ℕ → Prop) [decidable_pred P] (h : ∃ (n : ℕ), P n) :

(enat.find P).dom

theorem enat.lt_find (P : ℕ → Prop) [decidable_pred P] (n : ℕ) (h : ∀ (m : ℕ), m ≤ n → ¬P m) :

↑n < enat.find P

theorem enat.lt_find_iff (P : ℕ → Prop) [decidable_pred P] (n : ℕ) :

↑n < enat.find P ↔ ∀ (m : ℕ), m ≤ n → ¬P m

theorem enat.find_le (P : ℕ → Prop) [decidable_pred P] (n : ℕ) (h : P n) :

enat.find P ≤ ↑n

theorem enat.find_eq_top_iff (P : ℕ → Prop) [decidable_pred P] :

enat.find P = ⊤ ↔ ∀ (n : ℕ), ¬P n

@[protected, instance]

noncomputable def enat.linear_ordered_add_comm_monoid_with_top :

linear_ordered_add_comm_monoid_with_top enat

Equations

enat.linear_ordered_add_comm_monoid_with_top = {le := linear_order.le enat.linear_order, lt := linear_order.lt enat.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := linear_order.decidable_le enat.linear_order, decidable_eq := linear_order.decidable_eq enat.linear_order, decidable_lt := linear_order.decidable_lt enat.linear_order, max := max enat.linear_order, max_def := _, min := min enat.linear_order, min_def := _, 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 := _, nsmul := ordered_add_comm_monoid.nsmul enat.ordered_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, add_le_add_left := _, top := order_top.top enat.order_top, le_top := _, top_add' := enat.top_add}