Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-03 09:21 53c15319

View on Github →

feat(geometry/manifold/smooth_manifold_with_corners): product of smooth manifolds with corners (#3250)

Estimated changes

Modified src/analysis/calculus/times_cont_diff.lean

added theorem times_cont_diff_on.map_prod

added theorem times_cont_diff_on_fst

added theorem times_cont_diff_on_snd

Modified src/data/prod.lean

modified theorem prod.map_fst'

modified theorem prod.map_fst

modified theorem prod.map_snd'

modified theorem prod.map_snd

added theorem prod_map

Modified src/geometry/manifold/basic_smooth_bundle.lean

modified theorem basic_smooth_bundle_core.mem_atlas_iff

Modified src/geometry/manifold/charted_space.lean

added def model_prod

added theorem model_prod_range_prod_id

added theorem prod_charted_space_chart_at

Modified src/geometry/manifold/mfderiv.lean

modified theorem tangent_map_chart_symm

Modified src/geometry/manifold/smooth_manifold_with_corners.lean

added theorem model_with_corners_prod_coe

added theorem model_with_corners_prod_coe_symm

added theorem model_with_corners_prod_to_local_equiv

added theorem times_cont_diff_groupoid_prod