Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-23 22:04 604699b1

View on Github →

feat(data|set_theory): various new lemmas (#1466)

  • various changes
  • move section on map down I need some lemmas about nth for maps, and this seemed like the nicest way to do it
  • some lemmas
  • replace app by append in names
  • lemmas from various proving grounds problems
  • sanity_check on list.basic
  • small fixes in ordinal and cardinal also open namespace equiv in ordinal
  • small changes
  • add docstring
  • fix
  • rename variable
  • simp caused a problem
  • update docstring
  • fix last two comments

Estimated changes

added theorem lt_one_add
added theorem fin.coe_one
added theorem fin.coe_two
added theorem fin.coe_zero
modified theorem fin.injective_cast_le
added theorem fin.injective_val
added theorem fin.val_one
added theorem fin.val_two
modified theorem list.append_sublist_append
added theorem list.append_subset_iff
modified theorem list.bind_append
modified theorem list.bind_ret_eq_map
modified theorem list.chain'.iff_mem
added theorem list.doubleton_eq
added theorem list.empty_eq
modified theorem list.ilast'_mem
added theorem list.injective_length
added theorem list.injective_map_iff
added theorem list.insert_neg
added theorem list.insert_pos
added theorem list.join_join
modified theorem list.length_attach
modified theorem list.length_insert_of_mem
modified theorem list.map_eq_map
added theorem list.map_eq_map_iff
added theorem list.map_subset_iff
deleted theorem list.nodup_app_comm
added theorem list.nodup_append_comm
modified theorem list.nodup_append_of_nodup
modified theorem list.nth_le_attach
added theorem list.nth_le_map_rev
deleted theorem list.pairwise_app_comm
modified theorem list.rel_filter_map
added theorem list.singleton_eq
added theorem nat.pred_eq_succ_iff
added theorem set.set_of_app_iff
added theorem subtype.forall'
added theorem cardinal.mk_sum_compl
added theorem cardinal.add_eq_left
added theorem cardinal.add_eq_right
deleted theorem cardinal.aleph_is_limit
added theorem cardinal.le_mul_left
added theorem cardinal.le_mul_right
added theorem cardinal.mul_eq_left
added theorem cardinal.mul_eq_right
modified theorem cardinal.pow_le
added theorem ordinal.bsup_id
added theorem ordinal.lt_bsup
added theorem ordinal.nfp_eq_self
modified def principal_seg.lt_le
modified theorem principal_seg.lt_le_top