Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-17 15:19 2bc9354b

View on Github →

feat(data/nat/enat): extended natural numbers (#522)

Estimated changes

Created data/nat/enat.lean

added theorem enat.add_top

added theorem enat.coe_add

added theorem enat.coe_add_get

added theorem enat.coe_get

added theorem enat.coe_inj

added theorem enat.coe_le_coe

added theorem enat.coe_lt_coe

added theorem enat.coe_lt_top

added theorem enat.coe_one

added theorem enat.coe_zero

added theorem enat.dom_of_le_some

added theorem enat.get_add

added theorem enat.get_le_get

added theorem enat.get_one

added theorem enat.get_zero

added theorem enat.inf_eq_min

added theorem enat.pos_iff_one_le

added theorem enat.sup_eq_max

added theorem enat.top_add

added def enat

Modified data/pfun.lean

added theorem roption.get_eq_iff_eq_some

added def roption.get_or_else

added theorem roption.get_or_else_none

added theorem roption.get_or_else_some

added theorem roption.get_some

added theorem roption.some_get

added theorem roption.some_inj