Commit 2022-12-16 03:51 29f7ec5d

View on Github →

feat: port Data.Part (#1007) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Part.lean

added theorem Part.Dom.of_bind

added theorem Part.Mem.left_unique

added theorem Part.append_def

added theorem Part.append_get_eq

added theorem Part.append_mem_append

added def Part.assert

added theorem Part.assert_defined

added theorem Part.assert_neg

added theorem Part.assert_pos

added theorem Part.bind_assoc

added theorem Part.bind_defined

added theorem Part.bind_dom

added theorem Part.bind_eq_bind

added theorem Part.bind_le

added theorem Part.bind_map

added theorem Part.bind_none

added theorem Part.bind_of_mem

added theorem Part.bind_some

added theorem Part.bind_some_eq_map

added theorem Part.bind_some_right

added theorem Part.bind_toOption

added theorem Part.coe_none

added theorem Part.coe_some

added theorem Part.div_def

added theorem Part.div_get_eq

added theorem Part.div_mem_div

added theorem Part.dom_iff_mem

added theorem Part.elim_toOption

added theorem Part.eq_get_iff_mem

added theorem Part.eq_none_iff'

added theorem Part.eq_none_iff

added theorem Part.eq_none_or_eq_some

added theorem Part.eq_some_iff

added theorem Part.eta

added theorem Part.ext'

added theorem Part.ext

added def Part.getOrElse

added theorem Part.getOrElse_none

added theorem Part.getOrElse_of_dom

added theorem Part.getOrElse_of_not_dom

added theorem Part.getOrElse_some

added theorem Part.get_eq_get_of_eq

added theorem Part.get_eq_iff_eq_some

added theorem Part.get_eq_iff_mem

added theorem Part.get_eq_of_mem

added theorem Part.get_mem

added theorem Part.get_some

added theorem Part.inter_def

added theorem Part.inter_get_eq

added theorem Part.inter_mem_inter

added theorem Part.inv_def

added theorem Part.inv_mem_inv

added theorem Part.inv_some

added theorem Part.le_total_of_le_of_le

added theorem Part.left_dom_of_append_dom

added theorem Part.left_dom_of_div_dom

added theorem Part.left_dom_of_inter_dom

added theorem Part.left_dom_of_mod_dom

added theorem Part.left_dom_of_mul_dom

added theorem Part.left_dom_of_sdiff_dom

added theorem Part.left_dom_of_union_dom

added def Part.map

added theorem Part.map_bind

added theorem Part.map_eq_map

added theorem Part.map_id'

added theorem Part.map_map

added theorem Part.map_none

added theorem Part.map_some

added theorem Part.mem_assert

added theorem Part.mem_assert_iff

added theorem Part.mem_bind

added theorem Part.mem_bind_iff

added theorem Part.mem_coe

added theorem Part.mem_eq

added theorem Part.mem_map

added theorem Part.mem_map_iff

added theorem Part.mem_mk_iff

added theorem Part.mem_ofOption

added theorem Part.mem_restrict

added theorem Part.mem_some

added theorem Part.mem_some_iff

added theorem Part.mem_toOption

added theorem Part.mem_unique

added theorem Part.mod_def

added theorem Part.mod_get_eq

added theorem Part.mod_mem_mod

added theorem Part.mul_def

added theorem Part.mul_get_eq

added theorem Part.mul_mem_mul

added theorem Part.ne_none_iff

added def Part.none

added theorem Part.none_ne_some

added theorem Part.none_to_option

added theorem Part.not_mem_none

added theorem Part.not_none_dom

added def Part.ofOption

added theorem Part.ofOption_dom

added theorem Part.ofOption_eq_get

added theorem Part.of_toOption

added theorem Part.one_def

added theorem Part.one_mem_one

added theorem Part.pure_eq_some

added def Part.restrict

added theorem Part.ret_eq_some

added theorem Part.right_dom_of_append_dom

added theorem Part.right_dom_of_div_dom

added theorem Part.right_dom_of_inter_dom

added theorem Part.right_dom_of_mod_dom

added theorem Part.right_dom_of_mul_dom

added theorem Part.right_dom_of_sdiff_dom

added theorem Part.right_dom_of_union_dom

added theorem Part.sdiff_def

added theorem Part.sdiff_get_eq

added theorem Part.sdiff_mem_sdiff

added def Part.some

added theorem Part.some_append_some

added theorem Part.some_div_some

added theorem Part.some_dom

added theorem Part.some_get

added theorem Part.some_inj

added theorem Part.some_injective

added theorem Part.some_inter_some

added theorem Part.some_mod_some

added theorem Part.some_mul_some

added theorem Part.some_ne_none

added theorem Part.some_sdiff_some

added theorem Part.some_to_option

added theorem Part.some_union_some

added def Part.toOption

added theorem Part.toOption_eq_none_iff

added theorem Part.toOption_eq_some_iff

added theorem Part.to_ofOption

added theorem Part.union_def

added theorem Part.union_get_eq

added theorem Part.union_mem_union

added structure Part.{u}