Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smooth_on.prod_mk_space

Modification history

2021-03-15 15:39
src/geometry/manifold/times_cont_mdiff.lean
chore(geometry/manifold/times_cont_mdiff): add `prod_mk_space` versions of `prod_mk` lemmas (#6681) …
Added smooth_on.prod_mk_spaceView on Github →