Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-07 10:15 f063d0c6

View on Github →

feat(geometry/manifold/tangent_bundle): the tangent_bundle is a topological_vector_bundle (#8295)

Estimated changes

Modified src/geometry/manifold/cont_mdiff.lean

deleted theorem basic_smooth_bundle_core.cont_mdiff_at_proj

deleted theorem basic_smooth_bundle_core.cont_mdiff_on_proj

deleted theorem basic_smooth_bundle_core.cont_mdiff_proj

deleted theorem basic_smooth_bundle_core.cont_mdiff_within_at_proj

deleted theorem basic_smooth_bundle_core.smooth_at_proj

deleted theorem basic_smooth_bundle_core.smooth_const_section

deleted theorem basic_smooth_bundle_core.smooth_on_proj

deleted theorem basic_smooth_bundle_core.smooth_proj

deleted theorem basic_smooth_bundle_core.smooth_within_at_proj

added theorem basic_smooth_vector_bundle_core.cont_mdiff_at_proj

added theorem basic_smooth_vector_bundle_core.cont_mdiff_on_proj

added theorem basic_smooth_vector_bundle_core.cont_mdiff_proj

added theorem basic_smooth_vector_bundle_core.cont_mdiff_within_at_proj

added theorem basic_smooth_vector_bundle_core.smooth_at_proj

added theorem basic_smooth_vector_bundle_core.smooth_const_section

added theorem basic_smooth_vector_bundle_core.smooth_on_proj

added theorem basic_smooth_vector_bundle_core.smooth_proj

added theorem basic_smooth_vector_bundle_core.smooth_within_at_proj

deleted def tangent_bundle.zero_section

Modified src/geometry/manifold/mfderiv.lean

Renamed src/geometry/manifold/basic_smooth_bundle.lean to src/geometry/manifold/tangent_bundle.lean

deleted theorem basic_smooth_bundle_core.base_set

deleted def basic_smooth_bundle_core.chart

deleted theorem basic_smooth_bundle_core.chart_source

deleted theorem basic_smooth_bundle_core.chart_target

deleted theorem basic_smooth_bundle_core.coe_chart_at_fst

deleted theorem basic_smooth_bundle_core.coe_chart_at_symm_fst

deleted theorem basic_smooth_bundle_core.mem_atlas_iff

deleted theorem basic_smooth_bundle_core.mem_chart_source_iff

deleted theorem basic_smooth_bundle_core.mem_chart_target_iff

deleted def basic_smooth_bundle_core.to_topological_fiber_bundle_core

deleted structure basic_smooth_bundle_core

added theorem basic_smooth_vector_bundle_core.base_set

added def basic_smooth_vector_bundle_core.chart

added theorem basic_smooth_vector_bundle_core.chart_source

added theorem basic_smooth_vector_bundle_core.chart_target

added theorem basic_smooth_vector_bundle_core.coe_chart_at_fst

added theorem basic_smooth_vector_bundle_core.coe_chart_at_symm_fst

added theorem basic_smooth_vector_bundle_core.mem_atlas_iff

added theorem basic_smooth_vector_bundle_core.mem_chart_source_iff

added theorem basic_smooth_vector_bundle_core.mem_chart_target_iff

added theorem basic_smooth_vector_bundle_core.target

added def basic_smooth_vector_bundle_core.to_topological_vector_bundle_core

added structure basic_smooth_vector_bundle_core

modified def tangent_bundle

modified def tangent_bundle_core

modified def tangent_space

deleted def trivial_basic_smooth_bundle_core

added def trivial_basic_smooth_vector_bundle_core

Modified src/topology/vector_bundle.lean

added theorem topological_vector_bundle_core.base_set_at

added theorem topological_vector_bundle_core.local_triv_apply

added theorem topological_vector_bundle_core.local_triv_at_def

added theorem topological_vector_bundle_core.local_triv_symm_fst

added theorem topological_vector_bundle_core.mem_local_triv_at_base_set

modified theorem topological_vector_bundle_core.mem_local_triv_source

added theorem topological_vector_bundle_core.mem_local_triv_target

modified theorem topological_vector_bundle_core.mem_source_at

added def topological_vector_bundle_core.total_space

added def trivial_topological_vector_bundle_core