Commit 2023-03-07 19:08 be2c24f5

View on Github →

feat(geometry/manifold/vector_bundle/basic): smooth vector bundles (#17611) Definition of smooth vector bundle, and basic constructions (direct sum, pullback, core construction).

Estimated changes

Modified src/geometry/manifold/cont_mdiff.lean

added theorem cont_mdiff.clm_apply

modified theorem cont_mdiff.clm_comp

added theorem cont_mdiff.clm_prod_map

added theorem cont_mdiff_at.clm_apply

modified theorem cont_mdiff_at.clm_comp

added theorem cont_mdiff_at.clm_prod_map

added theorem cont_mdiff_on.clm_apply

modified theorem cont_mdiff_on.clm_comp

added theorem cont_mdiff_on.clm_prod_map

added theorem cont_mdiff_within_at.clm_apply

modified theorem cont_mdiff_within_at.clm_comp

added theorem cont_mdiff_within_at.clm_prod_map

Modified src/geometry/manifold/cont_mdiff_map.lean

Modified src/geometry/manifold/local_invariant_properties.lean

Created src/geometry/manifold/vector_bundle/basic.lean

Renamed src/geometry/manifold/vector_bundle.lean to src/geometry/manifold/vector_bundle/fiberwise_linear.lean

added theorem mem_smooth_fiberwise_linear_iff

Created src/geometry/manifold/vector_bundle/pullback.lean

Modified src/topology/fiber_bundle/basic.lean

Modified src/topology/fiber_bundle/constructions.lean

Modified src/topology/fiber_bundle/is_homeomorphic_trivial_bundle.lean

Modified src/topology/fiber_bundle/trivialization.lean

Modified src/topology/vector_bundle/basic.lean

added theorem trivialization.apply_symm_apply_eq_coord_changeL

added theorem trivialization.coe_coord_changeL'

added theorem trivialization.symm_coord_changeL

Modified src/topology/vector_bundle/constructions.lean

added theorem trivialization.coord_changeL_prod

Modified src/topology/vector_bundle/hom.lean