Mathlib v3 is deprecated. Go to Mathlib v4

Def continuous_map.prod_map

Modification history

2022-07-18 12:17
src/topology/continuous_function/basic.lean
feat(topology): basic simplification lemmas for `continuous_map`s (#15102) …
Modified continuous_map.prod_mapView on Github →
2021-12-30 14:54
src/topology/continuous_function/basic.lean
feat(topology/homotopy): Add homotopy product (#10946) …
Modified continuous_map.prod_mapView on Github →
2021-11-30 13:24
src/topology/continuous_function/basic.lean
feat(topology/[continuous_function, path_connected]): add bundled versions of prod_mk and prod_map (#10512) …
Added continuous_map.prod_mapView on Github →