Commit 2023-02-06 08:29 60855258

View on Github →

feat: port Data.Nat.PartENat (#1892) port of data.net.part_enat

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ENat/Basic.lean

deleted def ENat.ofNat

Created Mathlib/Data/Nat/PartENat.lean

added theorem PartENat.add_eq_top_iff

added theorem PartENat.add_one_le_iff_lt

added theorem PartENat.add_one_le_of_lt

added theorem PartENat.add_top

added theorem PartENat.coe_add_get

added theorem PartENat.coe_coeHom

added theorem PartENat.coe_le_coe

added theorem PartENat.coe_le_iff

added theorem PartENat.coe_lt_coe

added theorem PartENat.coe_lt_iff

added theorem PartENat.dom_natCast

added theorem PartENat.dom_of_le_natCast

added theorem PartENat.dom_of_le_of_dom

added theorem PartENat.dom_of_le_some

added theorem PartENat.dom_of_lt

added theorem PartENat.dom_some

added theorem PartENat.eq_top_iff_forall_le

added theorem PartENat.eq_top_iff_forall_lt

added def PartENat.find

added theorem PartENat.find_dom

added theorem PartENat.find_eq_top_iff

added theorem PartENat.find_get

added theorem PartENat.find_le

added theorem PartENat.get_add

added theorem PartENat.get_eq_iff_eq_coe

added theorem PartENat.get_le_get

added theorem PartENat.get_natCast'

added theorem PartENat.get_natCast

added theorem PartENat.get_one

added theorem PartENat.get_zero

added theorem PartENat.le_coe_iff

added theorem PartENat.le_def

added theorem PartENat.le_of_lt_add_one

added theorem PartENat.lt_add_one

added theorem PartENat.lt_add_one_iff_lt

added theorem PartENat.lt_coe_iff

added theorem PartENat.lt_def

added theorem PartENat.lt_find

added theorem PartENat.lt_find_iff

added theorem PartENat.lt_wf

added def PartENat.natCast_AddMonoidHom

added theorem PartENat.natCast_get

added theorem PartENat.natCast_inj

added theorem PartENat.natCast_lt_top

added theorem PartENat.natCast_ne_top

added theorem PartENat.ne_top_iff

added theorem PartENat.ne_top_iff_dom

added theorem PartENat.ne_top_of_lt

added theorem PartENat.ne_zero_iff

added theorem PartENat.not_dom_iff_eq_top

added theorem PartENat.not_isMax_natCast

added def PartENat.ofENat

added theorem PartENat.ofENat_none

added theorem PartENat.ofENat_some

added theorem PartENat.pos_iff_one_le

added def PartENat.some

added theorem PartENat.some_eq_natCast

added def PartENat.toWithTop

added theorem PartENat.toWithTop_add

added theorem PartENat.toWithTop_le

added theorem PartENat.toWithTop_lt

added theorem PartENat.toWithTop_natCast'

added theorem PartENat.toWithTop_natCast

added theorem PartENat.toWithTop_ofENat

added theorem PartENat.toWithTop_some

added theorem PartENat.toWithTop_top'

added theorem PartENat.toWithTop_top

added theorem PartENat.toWithTop_zero'

added theorem PartENat.toWithTop_zero

added theorem PartENat.top_add

added theorem PartENat.top_eq_none

added theorem PartENat.withTopEquiv_le

added theorem PartENat.withTopEquiv_lt

added theorem PartENat.withTopEquiv_natCast

added theorem PartENat.withTopEquiv_symm_coe

added theorem PartENat.withTopEquiv_symm_le

added theorem PartENat.withTopEquiv_symm_lt

added theorem PartENat.withTopEquiv_symm_top

added theorem PartENat.withTopEquiv_symm_zero

added theorem PartENat.withTopEquiv_top

added theorem PartENat.withTopEquiv_zero

added def PartENat