Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-03 15:36 3a58b50f

View on Github →

feat(data/equiv/basic): add more functions for equivalences between complex types (#1384)

Add more equiv combinators
Fix compile
Minor fixes
Update src/data/equiv/basic.lean Co-Authored-By: Chris Hughes 33847686+ChrisHughes24@users.noreply.github.com

Estimated changes

Modified src/data/equiv/basic.lean

deleted def equiv.equiv_fib

deleted def equiv.equiv_sigma_subtype

added def equiv.sigma_preimage_equiv

added def equiv.sigma_subtype_equiv_of_subset

added def equiv.sigma_subtype_preimage_equiv

added def equiv.sigma_subtype_preimage_equiv_subtype

modified def equiv.subtype_subtype_equiv_subtype

added def equiv.subtype_subtype_equiv_subtype_exists

added def equiv.subtype_subtype_equiv_subtype_inter

added def equiv.subtype_univ_equiv

Modified src/group_theory/coset.lean

Modified src/group_theory/sylow.lean

Modified src/set_theory/cardinal.lean

Modified src/set_theory/cofinality.lean