Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-05 00:46 62928251

View on Github →

feat(data/equiv/local_equiv): define local equivalences (#1359)

  • feat(data/equiv/local_equiv): define local equivalences
  • add doc
  • add extensionality attribute
  • sanity_check

Estimated changes

added def local_equiv.prod
added theorem local_equiv.refl_symm
added theorem local_equiv.refl_trans
added theorem local_equiv.restr_univ
added theorem local_equiv.symm_symm
added theorem local_equiv.trans_refl
added structure local_equiv