Commit 2021-07-09 12:40 5212f0ca

View on Github →

feat(Data/List/Basic): start porting from mathlib (#22)

  • feat(Data/List/Basic): start porting from mathlib
  • fix(Mathlib): fix order of imports
  • fixes from Gabriel
  • fix set syntax

Estimated changes

added theorem List.append_bind
added theorem List.append_eq_nil
added theorem List.append_subset_iff
added theorem List.ball_cons
added theorem List.ball_nil
added theorem List.bex_cons
added theorem List.bind_map
added theorem List.cons_bind
added theorem List.cons_ne_nil
added theorem List.cons_ne_self
added theorem List.cons_subset
added theorem List.cons_subset_cons
added theorem List.empty_eq
added theorem List.erase_append_left
added theorem List.erase_cons
added theorem List.erase_cons_head
added theorem List.erase_cons_tail
added theorem List.erase_eq_erasep
added theorem List.erase_nil
added theorem List.erase_of_not_mem
added theorem List.erase_subset
added def List.erasep
added theorem List.erasep_cons
added theorem List.erasep_map
added theorem List.erasep_nil
added theorem List.erasep_subset
added theorem List.exists_erase_eq
added theorem List.exists_of_erasep
added theorem List.exists_of_mem_map
added theorem List.forall_mem_append
added theorem List.forall_mem_cons
added theorem List.forall_mem_nil
added def List.insert
added theorem List.insert_of_mem
added theorem List.insert_of_not_mem
added theorem List.length_append
added theorem List.length_eq_one
added theorem List.length_eq_zero
added theorem List.length_map
added theorem List.length_pos_of_mem
added theorem List.length_singleton
added theorem List.map_append
added theorem List.map_eq_nil
added theorem List.map_id
added theorem List.map_map
added theorem List.map_singleton
added theorem List.map_subset
modified theorem List.mem_append
added theorem List.mem_append_eq
added theorem List.mem_append_left
added theorem List.mem_append_right
added theorem List.mem_bind_of_mem
added theorem List.mem_cons_eq
added theorem List.mem_cons_iff
added theorem List.mem_cons_of_mem
added theorem List.mem_cons_self
added theorem List.mem_erase_of_ne
added theorem List.mem_erasep_of_neg
added theorem List.mem_insert_iff
added theorem List.mem_insert_of_mem
added theorem List.mem_insert_self
added theorem List.mem_join_of_mem
added theorem List.mem_map_of_mem
added theorem List.mem_nil_iff
added theorem List.mem_of_mem_erase
added theorem List.mem_of_mem_erasep
added theorem List.mem_of_ne_of_mem
added theorem List.mem_singleton
added theorem List.mem_split
added theorem List.ne_nil_of_mem
added theorem List.nil_bind
added theorem List.nil_eq_append_iff
added theorem List.nil_subset
added theorem List.not_bex_nil
added theorem List.not_mem_append
added theorem List.not_mem_nil
added theorem List.singleton_append
added theorem List.subset.refl
added theorem List.subset.trans
added theorem List.subset_cons
added theorem List.subset_def
added theorem EqIffBeqTrue
added theorem NeqIffBeqFalse
added theorem and_imp
added theorem exists_eq'
added theorem exists_eq
added theorem exists_eq_left'
added theorem exists_eq_left
added theorem exists_eq_right
added theorem exists_false
added theorem exists_imp_distrib
added theorem forall_and_distrib
added theorem forall_eq
added theorem not.decidable_imp_symm
added theorem not_and
added theorem not_exists
added theorem not_forall
added theorem or_imp_distrib