mathlib
1b09efe3 - feat(topology/homeomorph): Product of sets is isomorphic to product of sets (#15664)

Commit

3 years ago

feat(topology/homeomorph): Product of sets is isomorphic to product of sets (#15664) This PR adds `homeomorph.set.prod`, analogous to `homeomorph.set.univ`.

Author

tb65536

Parents

7ad184e3

mathlib 1b09efe3 - feat(topology/homeomorph): Product of sets is isomorphic to product of sets (#15664)

mathlib
1b09efe3 - feat(topology/homeomorph): Product of sets is isomorphic to product of sets (#15664)