Commit 2021-06-09 11:55 f8294a67

View on Github →

feat (Data/Equiv/Basic): add equiv (#13)

  • add lemma macro
  • port init/function
  • equiv is an equivalence relation
  • a bit more equiv
  • functors send equivs to equivs
  • more tinkering
  • add changes suggested by review
  • add missing imports

Estimated changes

added theorem equiv.apply_symm_apply
added theorem equiv.coe_fn_mk
added def equiv.perm
added def equiv.refl
added theorem equiv.self_comp_symm
added def equiv.symm
added theorem equiv.symm_apply_apply
added theorem equiv.symm_comp_self
added def equiv.trans
added structure equiv
added theorem Functor.map_map
added def Function.app
added theorem Function.bijective_id
added def Function.combine
added theorem Function.comp.assoc
added theorem Function.comp.left_id
added theorem Function.comp.right_id
added theorem Function.comp_app
added def Function.curry
added theorem Function.curry_uncurry
added theorem Function.injective_id
added theorem Function.left_id
added def Function.on_fun
added theorem Function.right_id
added theorem Function.surjective_id
added def Function.swap
added def Function.uncurry
added theorem Function.uncurry_curry