Commit 2023-06-24 19:46 f272aa0a

View on Github →

feat: port Geometry.Manifold.VectorBundle.Tangent (#5448)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Data/Bundle.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem ModelProd.ext

Created Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean

added theorem TangentBundle.chartAt_toLocalEquiv

added theorem TangentBundle.coe_chartAt_fst

added theorem TangentBundle.coe_chartAt_symm_fst

added theorem TangentBundle.continuousLinearMapAt_model_space

added theorem TangentBundle.coordChange_model_space

added theorem TangentBundle.mem_chart_source_iff

added theorem TangentBundle.mem_chart_target_iff

added theorem TangentBundle.symmL_model_space

added theorem TangentBundle.trivializationAt_apply

added theorem TangentBundle.trivializationAt_baseSet

added theorem TangentBundle.trivializationAt_continuousLinearMapAt

added theorem TangentBundle.trivializationAt_eq_localTriv

added theorem TangentBundle.trivializationAt_fst

added theorem TangentBundle.trivializationAt_source

added theorem TangentBundle.trivializationAt_symmL

added theorem TangentBundle.trivializationAt_target

added def TangentBundle

added def TangentSpace

added theorem contDiffOn_fderiv_coord_change

added theorem inCoordinates_tangent_bundle_core_model_space

added def inTangentCoordinates

added theorem inTangentCoordinates_eq

added theorem inTangentCoordinates_model_space

added def tangentBundleCore

added theorem tangentBundleCore_baseSet

added theorem tangentBundleCore_coordChange_achart

added theorem tangentBundleCore_coordChange_model_space

added def tangentBundleModelSpaceHomeomorph

added theorem tangentBundleModelSpaceHomeomorph_coe

added theorem tangentBundleModelSpaceHomeomorph_coe_symm

added theorem tangentBundle_model_space_chartAt

added theorem tangentBundle_model_space_coe_chartAt

added theorem tangentBundle_model_space_coe_chartAt_symm

Modified Mathlib/Topology/FiberBundle/Basic.lean

Modified Mathlib/Topology/VectorBundle/Basic.lean