Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-20 09:15 804afcb0

View on Github →

feat(geometry/manifold/diffeomorph): some additions needed for smooth vector bundles (#14738)

Define diffeomorph.prod_comm, diffeomorph.prod_congr, diffeomorph.prod_assoc
Prove cont_mdiff_on.comp_cont_mdiff
In fiber_bundle, define some lemmas for local_triv_at that were already there for local_triv
Yes, this PR does a couple different things, but it is still very small
This is part of #14412

Estimated changes

Modified src/geometry/manifold/cont_mdiff.lean

added theorem cont_mdiff_on.comp_cont_mdiff

added theorem smooth_on.comp_smooth

Modified src/geometry/manifold/diffeomorph.lean

added theorem diffeomorph.coe_prod_comm

added theorem diffeomorph.coe_prod_congr

added def diffeomorph.prod_assoc

added def diffeomorph.prod_comm

added theorem diffeomorph.prod_comm_symm

added def diffeomorph.prod_congr

added theorem diffeomorph.prod_congr_symm

Modified src/topology/fiber_bundle.lean

modified theorem topological_fiber_bundle_core.local_triv_at_apply

added theorem topological_fiber_bundle_core.local_triv_at_apply_mk

added theorem topological_fiber_bundle_core.local_triv_symm_apply

deleted theorem topological_fiber_bundle_core.local_triv_symm_fst

added theorem topological_fiber_bundle_core.mem_local_triv_at_source

added theorem topological_fiber_bundle_core.mem_local_triv_at_target

Modified src/topology/vector_bundle/basic.lean

modified theorem topological_vector_bundle_core.local_triv_at_apply

added theorem topological_vector_bundle_core.local_triv_at_apply_mk

added def topological_vector_bundle_core.to_topological_fiber_bundle_core

deleted def topological_vector_bundle_core.to_topological_vector_bundle_core