Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-14 11:14 dcf01308

View on Github →

feat(data/pequiv): partial equivalences (#1206)

  • feat(data/pequiv): partial equivalences
  • Update src/data/pequiv.lean Co-Authored-By: Floris van Doorn fpvdoorn@gmail.com
  • use notation

Estimated changes

added def equiv.to_pequiv
added theorem equiv.to_pequiv_refl
added theorem equiv.to_pequiv_symm
added theorem equiv.to_pequiv_trans
added theorem pequiv.bot_apply
added theorem pequiv.bot_trans
added theorem pequiv.coe_mk_apply
added theorem pequiv.eq_some_iff
added theorem pequiv.ext
added theorem pequiv.ext_iff
added theorem pequiv.le_def
added theorem pequiv.mem_iff_mem
added theorem pequiv.mem_of_set_iff
added theorem pequiv.mem_single
added theorem pequiv.mem_single_iff
added theorem pequiv.mem_trans
added def pequiv.of_set
added theorem pequiv.of_set_eq_refl
added theorem pequiv.of_set_symm
added theorem pequiv.of_set_univ
added theorem pequiv.refl_apply
added theorem pequiv.refl_trans
added def pequiv.single
added theorem pequiv.single_apply
added theorem pequiv.symm_bot
added theorem pequiv.symm_injective
added theorem pequiv.symm_refl
added theorem pequiv.symm_refl_apply
added theorem pequiv.symm_single
added theorem pequiv.symm_symm
added theorem pequiv.symm_symm_apply
added theorem pequiv.symm_trans
added theorem pequiv.symm_trans_rev
added theorem pequiv.trans_assoc
added theorem pequiv.trans_bot
added theorem pequiv.trans_eq_none
added theorem pequiv.trans_eq_some
added theorem pequiv.trans_refl
added theorem pequiv.trans_symm
added structure pequiv