mathlib3 documentation

data.nat.part_enat

Natural numbers with infinity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The natural numbers and an extra top element ⊤. This implementation uses part ℕ as an implementation. Use ℕ∞ instead unless you care about computability.

Main definitions #

The following instances are defined:

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

Implementation details #

part_enat is defined to be part ℕ.

+ and ≤ are defined on part_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 part_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 #

part_enat, ℕ∞

source
def part_enat  :
Type

Type of natural numbers with infinity (⊤)

Equations
Instances for part_enat
source
def part_enat.some  :
ℕ → part_enat

The computable embedding ℕ → part_enat.

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

Equations
source
@[protected, instance]
def part_enat.has_zero  :
has_zero part_enat
Equations
source
@[protected, instance]
def part_enat.inhabited  :
inhabited part_enat
Equations
source
@[protected, instance]
def part_enat.has_one  :
has_one part_enat
Equations
source
@[protected, instance]
def part_enat.has_add  :
has_add part_enat
Equations
source
@[protected, instance]
def part_enat.dom.decidable (n : ℕ) :
decidable (part_enat.some n).dom
Equations
source
@[simp]
theorem part_enat.dom_some (x : ℕ) :
(part_enat.some x).dom
source
@[protected, instance]
def part_enat.add_comm_monoid  :
add_comm_monoid part_enat
Equations
source
@[protected, instance]
def part_enat.add_comm_monoid_with_one  :
add_comm_monoid_with_one part_enat
Equations
source
theorem part_enat.some_eq_coe (n : ℕ) :
part_enat.some n = ↑n
source
@[simp, norm_cast]
theorem part_enat.coe_inj {x y : ℕ} :
↑x = ↑y ↔ x = y
source
@[simp]
theorem part_enat.dom_coe (x : ℕ) :
↑x.dom
source
@[protected, instance]
def part_enat.part.dom.can_lift  :
can_lift part_enat ℕ coe part.dom
Equations
source
@[protected, instance]
def part_enat.has_le  :
has_le part_enat
Equations
source
@[protected, instance]
def part_enat.has_top  :
has_top part_enat
Equations
source
@[protected, instance]
def part_enat.has_bot  :
has_bot part_enat
Equations
source
@[protected, instance]
def part_enat.has_sup  :
has_sup part_enat
Equations
source
theorem part_enat.le_def (x y : part_enat) :
x ≤ y ↔ ∃ (h : y.dom → x.dom), ∀ (hy : y.dom), x.get _ ≤ y.get hy
source
@[protected]
theorem part_enat.cases_on' {P : part_enat → Prop} (a : part_enat) :
P ⊤ → (∀ (n : ℕ), P (part_enat.some n)) → P a
source
@[protected]
theorem part_enat.cases_on {P : part_enat → Prop} (a : part_enat) :
P ⊤ → (∀ (n : ℕ), P ↑n) → P a
source
@[simp]
theorem part_enat.top_add (x : part_enat) :
⊤ + x = ⊤
source
@[simp]
theorem part_enat.add_top (x : part_enat) :
x + ⊤ = ⊤
source
@[simp]
theorem part_enat.coe_get {x : part_enat} (h : x.dom) :
↑(x.get h) = x
source
@[simp, norm_cast]
theorem part_enat.get_coe' (x : ℕ) (h : ↑x.dom) :
↑x.get h = x
source
theorem part_enat.get_coe {x : ℕ} :
↑x.get _ = x
source
theorem part_enat.coe_add_get {x : ℕ} {y : part_enat} (h : (↑x + y).dom) :
(↑x + y).get h = x + y.get _
source
@[simp]
theorem part_enat.get_add {x y : part_enat} (h : (x + y).dom) :
(x + y).get h = x.get _ + y.get _
source
@[simp]
theorem part_enat.get_zero (h : 0.dom) :
0.get h = 0
source
@[simp]
theorem part_enat.get_one (h : 1.dom) :
1.get h = 1
source
theorem part_enat.get_eq_iff_eq_some {a : part_enat} {ha : a.dom} {b : ℕ} :
a.get ha = b ↔ a = part_enat.some b
source
theorem part_enat.get_eq_iff_eq_coe {a : part_enat} {ha : a.dom} {b : ℕ} :
a.get ha = b ↔ a = ↑b
source
theorem part_enat.dom_of_le_of_dom {x y : part_enat} :
x ≤ y → y.dom → x.dom
source
theorem part_enat.dom_of_le_some {x : part_enat} {y : ℕ} (h : x ≤ part_enat.some y) :
x.dom
source
theorem part_enat.dom_of_le_coe {x : part_enat} {y : ℕ} (h : x ≤ ↑y) :
x.dom
source
@[protected, instance]
def part_enat.decidable_le (x y : part_enat) [decidable x.dom] [decidable y.dom] :
decidable (x ≤ y)
Equations
source
def part_enat.coe_hom  :
ℕ →+ part_enat

The coercion ℕ → part_enat preserves 0 and addition.

Equations
source
@[simp]
theorem part_enat.coe_coe_hom  :
⇑part_enat.coe_hom = coe
source
@[protected, instance]
def part_enat.partial_order  :
partial_order part_enat
Equations
source
theorem part_enat.lt_def (x y : part_enat) :
x < y ↔ ∃ (hx : x.dom), ∀ (hy : y.dom), x.get hx < y.get hy
source
@[simp, norm_cast]
theorem part_enat.coe_le_coe {x y : ℕ} :
↑x ≤ ↑y ↔ x ≤ y
source
@[simp, norm_cast]
theorem part_enat.coe_lt_coe {x y : ℕ} :
↑x < ↑y ↔ x < y
source
@[simp]
theorem part_enat.get_le_get {x y : part_enat} {hx : x.dom} {hy : y.dom} :
x.get hx ≤ y.get hy ↔ x ≤ y
source
theorem part_enat.le_coe_iff (x : part_enat) (n : ℕ) :
x ≤ ↑n ↔ ∃ (h : x.dom), x.get h ≤ n
source
theorem part_enat.lt_coe_iff (x : part_enat) (n : ℕ) :
x < ↑n ↔ ∃ (h : x.dom), x.get h < n
source
theorem part_enat.coe_le_iff (n : ℕ) (x : part_enat) :
↑n ≤ x ↔ ∀ (h : x.dom), n ≤ x.get h
source
theorem part_enat.coe_lt_iff (n : ℕ) (x : part_enat) :
↑n < x ↔ ∀ (h : x.dom), n < x.get h
source
@[protected, instance]
def part_enat.ne_zero.one  :
ne_zero 1
source
@[protected, instance]
def part_enat.semilattice_sup  :
semilattice_sup part_enat
Equations
source
@[protected, instance]
def part_enat.order_bot  :
order_bot part_enat
Equations
source
@[protected, instance]
def part_enat.order_top  :
order_top part_enat
Equations
source
theorem part_enat.eq_zero_iff {x : part_enat} :
x = 0 ↔ x ≤ 0
source
theorem part_enat.ne_zero_iff {x : part_enat} :
x ≠ 0 ↔ ⊥ < x
source
theorem part_enat.dom_of_lt {x y : part_enat} :
x < y → x.dom
source
theorem part_enat.top_eq_none  :
⊤ = part.none
source
@[simp]
theorem part_enat.coe_lt_top (x : ℕ) :
↑x < ⊤
source
@[simp]
theorem part_enat.coe_ne_top (x : ℕ) :
↑x ≠ ⊤
source
theorem part_enat.not_is_max_coe (x : ℕ) :
¬is_max ↑x
source
theorem part_enat.ne_top_iff {x : part_enat} :
x ≠ ⊤ ↔ ∃ (n : ℕ), x = ↑n
source
theorem part_enat.ne_top_iff_dom {x : part_enat} :
x ≠ ⊤ ↔ x.dom
source
theorem part_enat.not_dom_iff_eq_top {x : part_enat} :
¬x.dom ↔ x = ⊤
source
theorem part_enat.ne_top_of_lt {x y : part_enat} (h : x < y) :
x ≠ ⊤
source
theorem part_enat.eq_top_iff_forall_lt (x : part_enat) :
x = ⊤ ↔ ∀ (n : ℕ), ↑n < x
source
theorem part_enat.eq_top_iff_forall_le (x : part_enat) :
x = ⊤ ↔ ∀ (n : ℕ), ↑n ≤ x
source
theorem part_enat.pos_iff_one_le {x : part_enat} :
0 < x ↔ 1 ≤ x
source
@[protected, instance]
def part_enat.has_le.le.is_total  :
is_total part_enat has_le.le
source
@[protected, instance]
noncomputable def part_enat.linear_order  :
linear_order part_enat
Equations
source
@[protected, instance]
def part_enat.bounded_order  :
bounded_order part_enat
Equations
source
@[protected, instance]
noncomputable def part_enat.lattice  :
lattice part_enat
Equations
source
@[protected, instance]
def part_enat.ordered_add_comm_monoid  :
ordered_add_comm_monoid part_enat
Equations
source
@[protected, instance]
def part_enat.canonically_ordered_add_monoid  :
canonically_ordered_add_monoid part_enat
Equations
source
theorem part_enat.eq_coe_sub_of_add_eq_coe {x y : part_enat} {n : ℕ} (h : x + y = ↑n) :
x = ↑(n - y.get _)
source
@[protected]
theorem part_enat.add_lt_add_right {x y z : part_enat} (h : x < y) (hz : z ≠ ⊤) :
x + z < y + z
source
@[protected]
theorem part_enat.add_lt_add_iff_right {x y z : part_enat} (hz : z ≠ ⊤) :
x + z < y + z ↔ x < y
source
@[protected]
theorem part_enat.add_lt_add_iff_left {x y z : part_enat} (hz : z ≠ ⊤) :
z + x < z + y ↔ x < y
source
@[protected]
theorem part_enat.lt_add_iff_pos_right {x y : part_enat} (hx : x ≠ ⊤) :
x < x + y ↔ 0 < y
source
theorem part_enat.lt_add_one {x : part_enat} (hx : x ≠ ⊤) :
x < x + 1
source
theorem part_enat.le_of_lt_add_one {x y : part_enat} (h : x < y + 1) :
x ≤ y
source
theorem part_enat.add_one_le_of_lt {x y : part_enat} (h : x < y) :
x + 1 ≤ y
source
theorem part_enat.add_one_le_iff_lt {x y : part_enat} (hx : x ≠ ⊤) :
x + 1 ≤ y ↔ x < y
source
theorem part_enat.coe_succ_le_iff {n : ℕ} {e : part_enat} :
↑(n.succ) ≤ e ↔ ↑n < e
source
theorem part_enat.lt_add_one_iff_lt {x y : part_enat} (hx : x ≠ ⊤) :
x < y + 1 ↔ x ≤ y
source
theorem part_enat.lt_coe_succ_iff_le {x : part_enat} {n : ℕ} (hx : x ≠ ⊤) :
x < ↑(n.succ) ↔ x ≤ ↑n
source
theorem part_enat.add_eq_top_iff {a b : part_enat} :
a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
source
@[protected]
theorem part_enat.add_right_cancel_iff {a b c : part_enat} (hc : c ≠ ⊤) :
a + c = b + c ↔ a = b
source
@[protected]
theorem part_enat.add_left_cancel_iff {a b c : part_enat} (ha : a ≠ ⊤) :
a + b = a + c ↔ b = c
source
def part_enat.to_with_top (x : part_enat) [decidable x.dom] :
ℕ∞

Computably converts an part_enat to a ℕ∞.

Equations
source
theorem part_enat.to_with_top_top  :
⊤.to_with_top = ⊤
source
@[simp]
theorem part_enat.to_with_top_top' {h : decidable ⊤.dom} :
⊤.to_with_top = ⊤
source
theorem part_enat.to_with_top_zero  :
0.to_with_top = 0
source
@[simp]
theorem part_enat.to_with_top_zero' {h : decidable 0.dom} :
0.to_with_top = 0
source
theorem part_enat.to_with_top_some (n : ℕ) :
(part_enat.some n).to_with_top = ↑n
source
theorem part_enat.to_with_top_coe (n : ℕ) {_x : decidable ↑n.dom} :
↑n.to_with_top = ↑n
source
@[simp]
theorem part_enat.to_with_top_coe' (n : ℕ) {h : decidable ↑n.dom} :
↑n.to_with_top = ↑n
source
@[simp]
theorem part_enat.to_with_top_le {x y : part_enat} [decidable x.dom] [decidable y.dom] :
x.to_with_top ≤ y.to_with_top ↔ x ≤ y
source
@[simp]
theorem part_enat.to_with_top_lt {x y : part_enat} [decidable x.dom] [decidable y.dom] :
x.to_with_top < y.to_with_top ↔ x < y
source
@[simp]
theorem part_enat.to_with_top_add {x y : part_enat} :
(x + y).to_with_top = x.to_with_top + y.to_with_top
source
noncomputable def part_enat.with_top_equiv  :
part_enat ≃ ℕ∞

equiv between part_enat and ℕ∞ (for the order isomorphism see with_top_order_iso).

Equations
source
@[simp]
theorem part_enat.with_top_equiv_top  :
⇑part_enat.with_top_equiv ⊤ = ⊤
source
@[simp]
theorem part_enat.with_top_equiv_coe (n : ℕ) :
⇑part_enat.with_top_equiv ↑n = ↑n
source
@[simp]
theorem part_enat.with_top_equiv_zero  :
⇑part_enat.with_top_equiv 0 = 0
source
@[simp]
theorem part_enat.with_top_equiv_le {x y : part_enat} :
⇑part_enat.with_top_equiv x ≤ ⇑part_enat.with_top_equiv y ↔ x ≤ y
source
@[simp]
theorem part_enat.with_top_equiv_lt {x y : part_enat} :
⇑part_enat.with_top_equiv x < ⇑part_enat.with_top_equiv y ↔ x < y
source
noncomputable def part_enat.with_top_order_iso  :
part_enat ≃o ℕ∞

to_with_top induces an order isomorphism between part_enat and ℕ∞.

Equations
source
@[simp]
theorem part_enat.with_top_equiv_symm_top  :
⇑(part_enat.with_top_equiv.symm) ⊤ = ⊤
source
@[simp]
theorem part_enat.with_top_equiv_symm_coe (n : ℕ) :
⇑(part_enat.with_top_equiv.symm) ↑n = ↑n
source
@[simp]
theorem part_enat.with_top_equiv_symm_zero  :
⇑(part_enat.with_top_equiv.symm) 0 = 0
source
@[simp]
theorem part_enat.with_top_equiv_symm_le {x y : ℕ∞} :
⇑(part_enat.with_top_equiv.symm) x ≤ ⇑(part_enat.with_top_equiv.symm) y ↔ x ≤ y
source
@[simp]
theorem part_enat.with_top_equiv_symm_lt {x y : ℕ∞} :
⇑(part_enat.with_top_equiv.symm) x < ⇑(part_enat.with_top_equiv.symm) y ↔ x < y
source
noncomputable def part_enat.with_top_add_equiv  :
part_enat ≃+ ℕ∞

to_with_top induces an additive monoid isomorphism between part_enat and ℕ∞.

Equations
source
theorem part_enat.lt_wf  :
well_founded has_lt.lt
source
@[protected, instance]
def part_enat.well_founded_lt  :
well_founded_lt part_enat
source
@[protected, instance]
def part_enat.has_lt.lt.is_well_order  :
is_well_order part_enat has_lt.lt
source
@[protected, instance]
def part_enat.has_well_founded  :
has_well_founded part_enat
Equations
source
def part_enat.find (P : ℕ → Prop) [decidable_pred P] :
part_enat

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

Equations
source
@[simp]
theorem part_enat.find_get (P : ℕ → Prop) [decidable_pred P] (h : (part_enat.find P).dom) :
(part_enat.find P).get h = nat.find h
source
theorem part_enat.find_dom (P : ℕ → Prop) [decidable_pred P] (h : ∃ (n : ℕ), P n) :
(part_enat.find P).dom
source
theorem part_enat.lt_find (P : ℕ → Prop) [decidable_pred P] (n : ℕ) (h : ∀ (m : ℕ), m ≤ n → ¬P m) :
↑n < part_enat.find P
source
theorem part_enat.lt_find_iff (P : ℕ → Prop) [decidable_pred P] (n : ℕ) :
↑n < part_enat.find P ↔ ∀ (m : ℕ), m ≤ n → ¬P m
source
theorem part_enat.find_le (P : ℕ → Prop) [decidable_pred P] (n : ℕ) (h : P n) :
part_enat.find P ≤ ↑n
source
theorem part_enat.find_eq_top_iff (P : ℕ → Prop) [decidable_pred P] :
part_enat.find P = ⊤ ↔ ∀ (n : ℕ), ¬P n
source
@[protected, instance]
noncomputable def part_enat.linear_ordered_add_comm_monoid_with_top  :
linear_ordered_add_comm_monoid_with_top part_enat
Equations
source
@[protected, instance]
noncomputable def part_enat.complete_linear_order  :
complete_linear_order part_enat
Equations