Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smooth_within_at.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_within_at.prod_mk_space View on Github →