basic): add lemmas characterising `equiv.Pi_congr` and `equiv.Pi_congr'` (#10432)

Commit

4 years ago

feat(data/equiv/basic): add lemmas characterising `equiv.Pi_congr` and `equiv.Pi_congr'` (#10432) Formalized as part of the Sphere Eversion project.

Author

ocfnash

Parents