mathlib docs: data.nat.enat

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}

source

@[instance]

def enat.has_le :

has_le enat

Equations

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

source

@[instance]

def enat.has_top :

has_top enat

Equations

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

source

@[instance]

def enat.has_bot :

has_bot enat

Equations

enat.has_bot = {bot := 0}

source

@[instance]

def enat.has_sup :

has_sup enat

Equations

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

source

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

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

source

@[simp]

theorem enat.top_add (x : enat) :

⊤ + x = ⊤

source

@[simp]

theorem enat.add_top (x : enat) :

x + ⊤ = ⊤

source

@[simp]

theorem enat.coe_zero :

↑0 = 0

source

@[simp]

theorem enat.coe_one :

↑1 = 1

source

@[simp]

theorem enat.coe_add (x y : ℕ) :

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

source

@[simp]

theorem enat.get_coe {x : ℕ} :

↑x.get true.intro = x

source

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

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

source

@[simp]

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

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

source

@[simp]

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

↑(x.get h) = x

source

@[simp]

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

0.get h = 0

source

@[simp]

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

1.get h = 1

source

theorem enat.dom_of_le_some {x : enat} {y : ℕ} :

x ≤ ↑y → x.dom

source

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

source

@[simp]

theorem enat.coe_le_coe {x y : ℕ} :

↑x ≤ ↑y ↔ x ≤ y

source

@[simp]

theorem enat.coe_lt_coe {x y : ℕ} :

↑x < ↑y ↔ x < y

source

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

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

source

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

source

@[instance]

def enat.order_top :

order_top enat

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}

source

theorem enat.top_eq_none :

⊤ = roption.none

source

theorem enat.coe_lt_top (x : ℕ) :

↑x < ⊤

source

@[simp]

theorem enat.coe_ne_top (x : ℕ) :

↑x ≠ ⊤

source

theorem enat.ne_top_iff {x : enat} :

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

source

theorem enat.ne_top_iff_dom {x : enat} :

x ≠ ⊤ ↔ x.dom

source

theorem enat.ne_top_of_lt {x y : enat} :

x < y → x ≠ ⊤

source

theorem enat.pos_iff_one_le {x : enat} :

0 < x ↔ 1 ≤ x

source

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

source

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

source

theorem enat.sup_eq_max {a b : enat} :

a ⊔ b = max a b

source

theorem enat.inf_eq_min {a b : enat} :

a ⊓ b = min a b

source

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

source

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

source

theorem enat.add_lt_add_right {x y z : enat} :

x < y → z ≠ ⊤ → x + z < y + z

source

theorem enat.add_lt_add_iff_right {x y z : enat} :

z ≠ ⊤ → (x + z < y + z ↔ x < y)

source

theorem enat.add_lt_add_iff_left {x y z : enat} :

z ≠ ⊤ → (z + x < z + y ↔ x < y)

source

theorem enat.lt_add_iff_pos_right {x y : enat} :

x ≠ ⊤ → (x < x + y ↔ 0 < y)

source

theorem enat.lt_add_one {x : enat} :

x ≠ ⊤ → x < x + 1

source

theorem enat.le_of_lt_add_one {x y : enat} :

x < y + 1 → x ≤ y

source

theorem enat.add_one_le_of_lt {x y : enat} :

x < y → x + 1 ≤ y

source

theorem enat.add_one_le_iff_lt {x y : enat} :

x ≠ ⊤ → (x + 1 ≤ y ↔ x < y)

source

theorem enat.lt_add_one_iff_lt {x y : enat} :

x ≠ ⊤ → (x < y + 1 ↔ x ≤ y)

source

theorem enat.add_eq_top_iff {a b : enat} :

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

source

theorem enat.add_right_cancel_iff {a b c : enat} :

c ≠ ⊤ → (a + c = b + c ↔ a = b)

source

theorem enat.add_left_cancel_iff {a b c : enat} :

a ≠ ⊤ → (a + b = a + c ↔ b = c)

source

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

with_top ℕ

Computably converts an enat to a with_top ℕ.

Equations

x.to_with_top = roption.to_option x

source

theorem enat.to_with_top_top :

⊤.to_with_top = ⊤

source

@[simp]

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

⊤.to_with_top = ⊤

source

theorem enat.to_with_top_zero :

0.to_with_top = 0

source

@[simp]

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

0.to_with_top = 0

source

theorem enat.to_with_top_coe (n : ℕ) :

↑n.to_with_top = ↑n

source

@[simp]

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

↑n.to_with_top = ↑n

source

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

source

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

source

def enat.with_top_equiv :

enat ≃ with_top ℕ

Order isomorphism between enat and with_top ℕ.

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 (option.some n) = ↑n
enat.with_top_equiv._match_1 option.none = ⊤