Commit 2021-07-27 17:57 fe7587ac

View on Github →

feat(Logic/Function/Basic) port most remaining items (#26)

  • port logic/function/basic.lean up to update_idem
  • fill in hole in forall_update_iff proof
  • Finish most of the rest of Function/Basic
  • use block tactic

Estimated changes

added theorem apply_dite
added theorem apply_ite
added theorem congr_arg2
added theorem dite_not
added theorem eq_rec_constant
added theorem exists_apply_eq_apply
added theorem forall_const
added theorem forall_prop_of_true
added theorem ite_not
added theorem Function.apply_update
added def Function.bicompl
added def Function.bicompr
added theorem Function.comp_update
added theorem Function.curry_apply
added theorem Function.eq_update_iff
added theorem Function.extend_apply
added theorem Function.extend_comp
added theorem Function.extend_def
added theorem Function.inv_fun_comp
added theorem Function.inv_fun_eq
added theorem Function.inv_fun_neg
added theorem Function.inv_fun_on_eq
added theorem Function.sometimes_eq
added theorem Function.surj_inv_eq
added theorem Function.uncurry_def
added def Function.update
added theorem Function.update_apply
added theorem Function.update_comm
added theorem Function.update_eq_iff
added theorem Function.update_idem
added theorem Function.update_noteq
added theorem Function.update_same
added def set.piecewise