basic): Show that `Pi_curry` is really just `sigma.curry` (#7497)

Commit

4 years ago

chore(data/equiv/basic): Show that `Pi_curry` is really just `sigma.curry` (#7497) Extracts some proofs to their own lemmas, and replaces definitions with existing ones.

Author

eric-wieser

Parents

9aed6c94

mathlib 6f27ef7c - chore(data/equiv/basic): Show that `Pi_curry` is really just `sigma.curry` (#7497)

mathlib
6f27ef7c - chore(data/equiv/basic): Show that `Pi_curry` is really just `sigma.curry` (#7497)