Commit 2026-02-27 16:42 fd11b7a3

View on Github →

chore: move Pretrivialization, Trivialization to the Bundle namespace (#31338) As suggested in #30083.

Estimated changes

Modified Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean

added theorem Bundle.Trivialization.mdifferentiable

deleted theorem Trivialization.mdifferentiable

Modified Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

added theorem Bundle.Trivialization.contMDiffAt_iff

added theorem Bundle.Trivialization.contMDiffAt_section_iff

added theorem Bundle.Trivialization.contMDiffOn

added theorem Bundle.Trivialization.contMDiffOn_iff

added theorem Bundle.Trivialization.contMDiffOn_section_baseSet_iff

added theorem Bundle.Trivialization.contMDiffOn_section_iff

added theorem Bundle.Trivialization.contMDiffOn_symm

added theorem Bundle.Trivialization.contMDiffOn_symm_trans

added theorem Bundle.Trivialization.contMDiffWithinAt_iff

added theorem Bundle.Trivialization.contMDiffWithinAt_section

added theorem Bundle.Trivialization.contMDiffWithinAt_snd_comp_iff₂

added theorem Bundle.Trivialization.contMDiff_iff

deleted theorem Trivialization.contMDiffAt_iff

deleted theorem Trivialization.contMDiffAt_section_iff

deleted theorem Trivialization.contMDiffOn

deleted theorem Trivialization.contMDiffOn_iff

deleted theorem Trivialization.contMDiffOn_section_baseSet_iff

deleted theorem Trivialization.contMDiffOn_section_iff

deleted theorem Trivialization.contMDiffOn_symm

deleted theorem Trivialization.contMDiffOn_symm_trans

deleted theorem Trivialization.contMDiffWithinAt_iff

deleted theorem Trivialization.contMDiffWithinAt_section

deleted theorem Trivialization.contMDiffWithinAt_snd_comp_iff₂

deleted theorem Trivialization.contMDiff_iff

Modified Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

added def Bundle.Trivialization.basisAt

added theorem Bundle.Trivialization.contMDiffOn_localFrame_baseSet

added theorem Bundle.Trivialization.eq_sum_localFrame_coeff_smul

added theorem Bundle.Trivialization.eventually_eq_localFrame_sum_coeff_smul

added theorem Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet

added def Bundle.Trivialization.localFrame

added theorem Bundle.Trivialization.localFrame_apply_of_mem_baseSet

added theorem Bundle.Trivialization.localFrame_apply_of_notMem

added def Bundle.Trivialization.localFrame_coeff

added theorem Bundle.Trivialization.localFrame_coeff_apply_of_mem_baseSet

added theorem Bundle.Trivialization.localFrame_coeff_apply_of_notMem_baseSet

added theorem Bundle.Trivialization.localFrame_coeff_congr

added theorem Bundle.Trivialization.localFrame_coeff_eq_coeff

deleted def Trivialization.basisAt

deleted theorem Trivialization.contMDiffOn_localFrame_baseSet

deleted theorem Trivialization.eq_sum_localFrame_coeff_smul

deleted theorem Trivialization.eventually_eq_localFrame_sum_coeff_smul

deleted theorem Trivialization.isLocalFrameOn_localFrame_baseSet

deleted def Trivialization.localFrame

deleted theorem Trivialization.localFrame_apply_of_mem_baseSet

deleted theorem Trivialization.localFrame_apply_of_notMem

deleted def Trivialization.localFrame_coeff

deleted theorem Trivialization.localFrame_coeff_apply_of_mem_baseSet

deleted theorem Trivialization.localFrame_coeff_apply_of_notMem_baseSet

deleted theorem Trivialization.localFrame_coeff_congr

deleted theorem Trivialization.localFrame_coeff_eq_coeff

Modified Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean

added theorem Bundle.Trivialization.mdifferentiableAt_section_iff

added theorem Bundle.Trivialization.mdifferentiableAt_snd_comp_iff₂

added theorem Bundle.Trivialization.mdifferentiableAt_totalSpace_iff

added theorem Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff

added theorem Bundle.Trivialization.mdifferentiableOn_section_iff

added theorem Bundle.Trivialization.mdifferentiableWithinAt_section_iff

added theorem Bundle.Trivialization.mdifferentiableWithinAt_snd_comp_iff₂

added theorem Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff

deleted theorem Trivialization.mdifferentiableAt_section_iff

deleted theorem Trivialization.mdifferentiableAt_snd_comp_iff₂

deleted theorem Trivialization.mdifferentiableAt_totalSpace_iff

deleted theorem Trivialization.mdifferentiableOn_section_baseSet_iff

deleted theorem Trivialization.mdifferentiableOn_section_iff

deleted theorem Trivialization.mdifferentiableWithinAt_section_iff

deleted theorem Trivialization.mdifferentiableWithinAt_snd_comp_iff₂

deleted theorem Trivialization.mdifferentiableWithinAt_totalSpace_iff

Modified Mathlib/Topology/Covering/Basic.lean

Modified Mathlib/Topology/Covering/Quotient.lean

Modified Mathlib/Topology/FiberBundle/Constructions.lean

added theorem Bundle.Trivialization.Prod.continuous_inv_fun

added theorem Bundle.Trivialization.Prod.continuous_to_fun

added theorem Bundle.Trivialization.Prod.left_inv

added theorem Bundle.Trivialization.Prod.right_inv

added def Bundle.Trivialization.Prod.toFun'

added theorem Bundle.Trivialization.prod_symm_apply

deleted theorem Trivialization.Prod.continuous_inv_fun

deleted theorem Trivialization.Prod.continuous_to_fun

deleted theorem Trivialization.Prod.left_inv

deleted theorem Trivialization.Prod.right_inv

deleted def Trivialization.Prod.toFun'

deleted theorem Trivialization.prod_symm_apply

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

added def Bundle.Pretrivialization.Trivialization.Simps.apply

added theorem Bundle.Pretrivialization.Trivialization.apply_mk_symm

added theorem Bundle.Pretrivialization.Trivialization.apply_symm_apply'

added theorem Bundle.Pretrivialization.Trivialization.apply_symm_apply

added def Bundle.Pretrivialization.Trivialization.clift

added theorem Bundle.Pretrivialization.Trivialization.clift_self

added theorem Bundle.Pretrivialization.Trivialization.coe_coe

added theorem Bundle.Pretrivialization.Trivialization.coe_coe_fst

added theorem Bundle.Pretrivialization.Trivialization.coe_fst'

added theorem Bundle.Pretrivialization.Trivialization.coe_fst

added theorem Bundle.Pretrivialization.Trivialization.coe_fst_eventuallyEq_proj'

added theorem Bundle.Pretrivialization.Trivialization.coe_fst_eventuallyEq_proj

added theorem Bundle.Pretrivialization.Trivialization.coe_mem_source

added theorem Bundle.Pretrivialization.Trivialization.coe_mk

added theorem Bundle.Pretrivialization.Trivialization.continuousAt_of_comp_left

added theorem Bundle.Pretrivialization.Trivialization.continuousAt_of_comp_right

added theorem Bundle.Pretrivialization.Trivialization.continuousAt_proj

added theorem Bundle.Pretrivialization.Trivialization.continuousOn_proj

added theorem Bundle.Pretrivialization.Trivialization.continuousOn_symm

added theorem Bundle.Pretrivialization.Trivialization.continuous_coordChange

added def Bundle.Pretrivialization.Trivialization.coordChange

added theorem Bundle.Pretrivialization.Trivialization.coordChangeHomeomorph_coe

added theorem Bundle.Pretrivialization.Trivialization.coordChange_apply_snd

added theorem Bundle.Pretrivialization.Trivialization.coordChange_coordChange

added theorem Bundle.Pretrivialization.Trivialization.coordChange_same

added theorem Bundle.Pretrivialization.Trivialization.coordChange_same_apply

added theorem Bundle.Pretrivialization.Trivialization.ext'

added theorem Bundle.Pretrivialization.Trivialization.frontier_preimage

added theorem Bundle.Pretrivialization.Trivialization.image_preimage_eq_prod_univ

added theorem Bundle.Pretrivialization.Trivialization.isImage_preimage_prod

added def Bundle.Pretrivialization.Trivialization.lift

added def Bundle.Pretrivialization.Trivialization.liftCM

added theorem Bundle.Pretrivialization.Trivialization.lift_self

added theorem Bundle.Pretrivialization.Trivialization.map_proj_nhds

added theorem Bundle.Pretrivialization.Trivialization.map_target

added theorem Bundle.Pretrivialization.Trivialization.mem_source

added theorem Bundle.Pretrivialization.Trivialization.mem_target

added theorem Bundle.Pretrivialization.Trivialization.mk_coordChange

added theorem Bundle.Pretrivialization.Trivialization.mk_mem_target

added theorem Bundle.Pretrivialization.Trivialization.mk_proj_snd'

added theorem Bundle.Pretrivialization.Trivialization.mk_proj_snd

added theorem Bundle.Pretrivialization.Trivialization.mk_symm

added theorem Bundle.Pretrivialization.Trivialization.nhds_eq_inf_comap

added def Bundle.Pretrivialization.Trivialization.preimageHomeomorph

added theorem Bundle.Pretrivialization.Trivialization.preimageHomeomorph_apply

added theorem Bundle.Pretrivialization.Trivialization.preimageHomeomorph_symm_apply

added def Bundle.Pretrivialization.Trivialization.preimageSingletonHomeomorph

added theorem Bundle.Pretrivialization.Trivialization.preimageSingletonHomeomorph_apply

added theorem Bundle.Pretrivialization.Trivialization.preimageSingletonHomeomorph_symm_apply

added theorem Bundle.Pretrivialization.Trivialization.preimage_subset_source

added theorem Bundle.Pretrivialization.Trivialization.proj_clift

added theorem Bundle.Pretrivialization.Trivialization.proj_lift

added theorem Bundle.Pretrivialization.Trivialization.proj_surjOn_baseSet

added theorem Bundle.Pretrivialization.Trivialization.proj_symm_apply'

added theorem Bundle.Pretrivialization.Trivialization.proj_symm_apply

added def Bundle.Pretrivialization.Trivialization.sourceHomeomorphBaseSetProd

added theorem Bundle.Pretrivialization.Trivialization.sourceHomeomorphBaseSetProd_apply

added theorem Bundle.Pretrivialization.Trivialization.sourceHomeomorphBaseSetProd_symm_apply

added theorem Bundle.Pretrivialization.Trivialization.source_inter_preimage_target_inter

added theorem Bundle.Pretrivialization.Trivialization.symm_apply

added theorem Bundle.Pretrivialization.Trivialization.symm_apply_apply

added theorem Bundle.Pretrivialization.Trivialization.symm_apply_apply_mk

added theorem Bundle.Pretrivialization.Trivialization.symm_apply_mk_proj

added theorem Bundle.Pretrivialization.Trivialization.symm_apply_of_notMem

added theorem Bundle.Pretrivialization.Trivialization.symm_coe_proj

added theorem Bundle.Pretrivialization.Trivialization.symm_proj_apply

added theorem Bundle.Pretrivialization.Trivialization.symm_trans_source_eq

added theorem Bundle.Pretrivialization.Trivialization.symm_trans_target_eq

added theorem Bundle.Pretrivialization.Trivialization.tendsto_nhds_iff

added def Bundle.Pretrivialization.Trivialization.toFun'

added def Bundle.Pretrivialization.Trivialization.toPretrivialization

added theorem Bundle.Pretrivialization.Trivialization.toPretrivialization_injective

added def Bundle.Pretrivialization.Trivialization.transFiberHomeomorph

added theorem Bundle.Pretrivialization.Trivialization.transFiberHomeomorph_apply

added structure Bundle.Pretrivialization.Trivialization

added theorem Bundle.Pretrivialization.apply_mk_symm

added theorem Bundle.Pretrivialization.apply_symm_apply'

added theorem Bundle.Pretrivialization.apply_symm_apply

added theorem Bundle.Pretrivialization.coe_coe

added theorem Bundle.Pretrivialization.coe_coe_fst

added theorem Bundle.Pretrivialization.coe_fst'

added theorem Bundle.Pretrivialization.coe_fst

added theorem Bundle.Pretrivialization.coe_mem_source

added theorem Bundle.Pretrivialization.coe_symm_of_notMem

added theorem Bundle.Pretrivialization.ext'

added theorem Bundle.Pretrivialization.ext

added theorem Bundle.Pretrivialization.mem_source

added theorem Bundle.Pretrivialization.mem_target

added theorem Bundle.Pretrivialization.mk_mem_target

added theorem Bundle.Pretrivialization.mk_proj_snd'

added theorem Bundle.Pretrivialization.mk_proj_snd

added theorem Bundle.Pretrivialization.mk_symm

added theorem Bundle.Pretrivialization.preimage_symm_proj_baseSet

added theorem Bundle.Pretrivialization.preimage_symm_proj_inter

added theorem Bundle.Pretrivialization.proj_surjOn_baseSet

added theorem Bundle.Pretrivialization.proj_symm_apply'

added theorem Bundle.Pretrivialization.proj_symm_apply

added def Bundle.Pretrivialization.setSymm

added theorem Bundle.Pretrivialization.symm_apply

added theorem Bundle.Pretrivialization.symm_apply_apply

added theorem Bundle.Pretrivialization.symm_apply_apply_mk

added theorem Bundle.Pretrivialization.symm_apply_mk_proj

added theorem Bundle.Pretrivialization.symm_apply_of_notMem

added theorem Bundle.Pretrivialization.symm_coe_proj

added theorem Bundle.Pretrivialization.symm_proj_apply

added theorem Bundle.Pretrivialization.symm_trans_source_eq

added theorem Bundle.Pretrivialization.symm_trans_symm

added theorem Bundle.Pretrivialization.symm_trans_target_eq

added theorem Bundle.Pretrivialization.target_inter_preimage_symm_source_eq

added def Bundle.Pretrivialization.toFun'

added theorem Bundle.Pretrivialization.toPartialEquiv_injective

added theorem Bundle.Pretrivialization.trans_source

added structure Bundle.Pretrivialization

deleted theorem Pretrivialization.apply_mk_symm

deleted theorem Pretrivialization.apply_symm_apply'

deleted theorem Pretrivialization.apply_symm_apply

deleted theorem Pretrivialization.coe_coe

deleted theorem Pretrivialization.coe_coe_fst

deleted theorem Pretrivialization.coe_fst'

deleted theorem Pretrivialization.coe_fst

deleted theorem Pretrivialization.coe_mem_source

deleted theorem Pretrivialization.coe_symm_of_notMem

deleted theorem Pretrivialization.ext'

deleted theorem Pretrivialization.ext

deleted theorem Pretrivialization.mem_source

deleted theorem Pretrivialization.mem_target

deleted theorem Pretrivialization.mk_mem_target

deleted theorem Pretrivialization.mk_proj_snd'

deleted theorem Pretrivialization.mk_proj_snd

deleted theorem Pretrivialization.mk_symm

deleted theorem Pretrivialization.preimage_symm_proj_baseSet

deleted theorem Pretrivialization.preimage_symm_proj_inter

deleted theorem Pretrivialization.proj_surjOn_baseSet

deleted theorem Pretrivialization.proj_symm_apply'

deleted theorem Pretrivialization.proj_symm_apply

deleted def Pretrivialization.setSymm

deleted theorem Pretrivialization.symm_apply

deleted theorem Pretrivialization.symm_apply_apply

deleted theorem Pretrivialization.symm_apply_apply_mk

deleted theorem Pretrivialization.symm_apply_mk_proj

deleted theorem Pretrivialization.symm_apply_of_notMem

deleted theorem Pretrivialization.symm_coe_proj

deleted theorem Pretrivialization.symm_proj_apply

deleted theorem Pretrivialization.symm_trans_source_eq

deleted theorem Pretrivialization.symm_trans_symm

deleted theorem Pretrivialization.symm_trans_target_eq

deleted theorem Pretrivialization.target_inter_preimage_symm_source_eq

deleted def Pretrivialization.toFun'

deleted theorem Pretrivialization.toPartialEquiv_injective

deleted theorem Pretrivialization.trans_source

deleted structure Pretrivialization

deleted def Trivialization.Simps.apply

deleted theorem Trivialization.apply_mk_symm

deleted theorem Trivialization.apply_symm_apply'

deleted theorem Trivialization.apply_symm_apply

deleted def Trivialization.clift

deleted theorem Trivialization.clift_self

deleted theorem Trivialization.coe_coe

deleted theorem Trivialization.coe_coe_fst

deleted theorem Trivialization.coe_fst'

deleted theorem Trivialization.coe_fst

deleted theorem Trivialization.coe_fst_eventuallyEq_proj'

deleted theorem Trivialization.coe_fst_eventuallyEq_proj

deleted theorem Trivialization.coe_mem_source

deleted theorem Trivialization.coe_mk

deleted theorem Trivialization.continuousAt_of_comp_left

deleted theorem Trivialization.continuousAt_of_comp_right

deleted theorem Trivialization.continuousAt_proj

deleted theorem Trivialization.continuousOn_proj

deleted theorem Trivialization.continuousOn_symm

deleted theorem Trivialization.continuous_coordChange

deleted def Trivialization.coordChange

deleted theorem Trivialization.coordChangeHomeomorph_coe

deleted theorem Trivialization.coordChange_apply_snd

deleted theorem Trivialization.coordChange_coordChange

deleted theorem Trivialization.coordChange_same

deleted theorem Trivialization.coordChange_same_apply

deleted theorem Trivialization.ext'

deleted theorem Trivialization.frontier_preimage

deleted theorem Trivialization.image_preimage_eq_prod_univ

deleted theorem Trivialization.isImage_preimage_prod

deleted def Trivialization.lift

deleted def Trivialization.liftCM

deleted theorem Trivialization.lift_self

deleted theorem Trivialization.map_proj_nhds

deleted theorem Trivialization.map_target

deleted theorem Trivialization.mem_source

deleted theorem Trivialization.mem_target

deleted theorem Trivialization.mk_coordChange

deleted theorem Trivialization.mk_mem_target

deleted theorem Trivialization.mk_proj_snd'

deleted theorem Trivialization.mk_proj_snd

deleted theorem Trivialization.mk_symm

deleted theorem Trivialization.nhds_eq_inf_comap

deleted def Trivialization.preimageHomeomorph

deleted theorem Trivialization.preimageHomeomorph_apply

deleted theorem Trivialization.preimageHomeomorph_symm_apply

deleted def Trivialization.preimageSingletonHomeomorph

deleted theorem Trivialization.preimageSingletonHomeomorph_apply

deleted theorem Trivialization.preimageSingletonHomeomorph_symm_apply

deleted theorem Trivialization.preimage_subset_source

deleted theorem Trivialization.proj_clift

deleted theorem Trivialization.proj_lift

deleted theorem Trivialization.proj_surjOn_baseSet

deleted theorem Trivialization.proj_symm_apply'

deleted theorem Trivialization.proj_symm_apply

deleted def Trivialization.sourceHomeomorphBaseSetProd

deleted theorem Trivialization.sourceHomeomorphBaseSetProd_apply

deleted theorem Trivialization.sourceHomeomorphBaseSetProd_symm_apply

deleted theorem Trivialization.source_inter_preimage_target_inter

deleted theorem Trivialization.symm_apply

deleted theorem Trivialization.symm_apply_apply

deleted theorem Trivialization.symm_apply_apply_mk

deleted theorem Trivialization.symm_apply_mk_proj

deleted theorem Trivialization.symm_apply_of_notMem

deleted theorem Trivialization.symm_coe_proj

deleted theorem Trivialization.symm_proj_apply

deleted theorem Trivialization.symm_trans_source_eq

deleted theorem Trivialization.symm_trans_target_eq

deleted theorem Trivialization.tendsto_nhds_iff

deleted def Trivialization.toFun'

deleted def Trivialization.toPretrivialization

deleted theorem Trivialization.toPretrivialization_injective

deleted def Trivialization.transFiberHomeomorph

deleted theorem Trivialization.transFiberHomeomorph_apply

deleted structure Trivialization

Modified Mathlib/Topology/VectorBundle/Basic.lean

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.apply_eq_prod_continuousLinearEquivAt

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.coe_continuousLinearEquivAt_eq

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.comp_continuousLinearEquivAt_eq_coord_change

added def Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.continuousLinearEquivAt

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.continuousLinearEquivAt_apply'

added def Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.continuousLinearMapAt

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.continuousLinearMapAt_symmL

added def Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.symmL

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.symmL_continuousLinearMapAt

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm

added theorem Bundle.Pretrivialization.Trivialization.Bundle.Trivialization.symm_continuousLinearEquivAt_eq

added def Bundle.Pretrivialization.Trivialization.Bundle.zeroSection

added theorem Bundle.Pretrivialization.Trivialization.Bundle.zeroSection_proj

added theorem Bundle.Pretrivialization.Trivialization.Bundle.zeroSection_snd

added def Bundle.Pretrivialization.Trivialization.ContinuousLinearMap.inCoordinates

added theorem Bundle.Pretrivialization.Trivialization.ContinuousLinearMap.inCoordinates_eq

added def Bundle.Pretrivialization.Trivialization.VectorBundleCore.Base

added def Bundle.Pretrivialization.Trivialization.VectorBundleCore.Fiber

added def Bundle.Pretrivialization.Trivialization.VectorBundleCore.Index

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.baseSet_at

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.coe_coordChange

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.continuous_proj

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.coordChange_linear_comp

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.isOpenMap_proj

added def Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTriv

added def Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTrivAt

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTrivAt_apply

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTrivAt_apply_mk

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTrivAt_def

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTriv_apply

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTriv_continuousLinearMapAt

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTriv_coordChange_eq

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTriv_symmL

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTriv_symm_apply

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.localTriv_symm_fst

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.mem_localTrivAt_baseSet

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.mem_localTriv_source

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.mem_localTriv_target

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.mem_source_at

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.mem_trivChange_source

added def Bundle.Pretrivialization.Trivialization.VectorBundleCore.toFiberBundleCore

added def Bundle.Pretrivialization.Trivialization.VectorBundleCore.trivChange

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.trivializationAt_continuousLinearMapAt

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.trivializationAt_coordChange_eq

added theorem Bundle.Pretrivialization.Trivialization.VectorBundleCore.trivializationAt_symmL

added structure Bundle.Pretrivialization.Trivialization.VectorBundleCore

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.continuousOn_coordChange

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.continuous_totalSpaceMk

added def Bundle.Pretrivialization.Trivialization.VectorPrebundle.coordChange

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.coordChange_apply

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.mem_trivialization_at_source

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.mk_coordChange

added def Bundle.Pretrivialization.Trivialization.VectorPrebundle.toFiberBundle

added def Bundle.Pretrivialization.Trivialization.VectorPrebundle.toFiberPrebundle

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.toVectorBundle

added theorem Bundle.Pretrivialization.Trivialization.VectorPrebundle.totalSpaceMk_preimage_source

added def Bundle.Pretrivialization.Trivialization.VectorPrebundle.totalSpaceTopology

added def Bundle.Pretrivialization.Trivialization.VectorPrebundle.trivializationOfMemPretrivializationAtlas

added structure Bundle.Pretrivialization.Trivialization.VectorPrebundle

added theorem Bundle.Pretrivialization.Trivialization.apply_symm_apply_eq_coordChangeL

added theorem Bundle.Pretrivialization.Trivialization.coe_coordChangeL'

added theorem Bundle.Pretrivialization.Trivialization.coe_coordChangeL

added theorem Bundle.Pretrivialization.Trivialization.coe_linearMapAt

added theorem Bundle.Pretrivialization.Trivialization.coe_linearMapAt_of_mem

added theorem Bundle.Pretrivialization.Trivialization.coe_symmₗ

added theorem Bundle.Pretrivialization.Trivialization.continuousOn_coordChange

added def Bundle.Pretrivialization.Trivialization.coordChangeL

added theorem Bundle.Pretrivialization.Trivialization.coordChangeL_apply'

added theorem Bundle.Pretrivialization.Trivialization.coordChangeL_apply

added theorem Bundle.Pretrivialization.Trivialization.coordChangeL_symm_apply

added def Bundle.Pretrivialization.Trivialization.linearEquivAt

added theorem Bundle.Pretrivialization.Trivialization.linearEquivAt_apply

added theorem Bundle.Pretrivialization.Trivialization.linearEquivAt_symm_apply

added theorem Bundle.Pretrivialization.Trivialization.linearMapAt_apply

added theorem Bundle.Pretrivialization.Trivialization.linearMapAt_def_of_mem

added theorem Bundle.Pretrivialization.Trivialization.linearMapAt_def_of_notMem

added theorem Bundle.Pretrivialization.Trivialization.linearMapAt_symmₗ

added theorem Bundle.Pretrivialization.Trivialization.mk_coordChangeL

added theorem Bundle.Pretrivialization.Trivialization.symm_coordChangeL

added theorem Bundle.Pretrivialization.Trivialization.symmₗ_linearMapAt

added def Bundle.Pretrivialization.Trivialization.trivialVectorBundleCore

added theorem Bundle.Pretrivialization.coe_linearMapAt

added theorem Bundle.Pretrivialization.coe_linearMapAt_of_mem

added theorem Bundle.Pretrivialization.linear

added def Bundle.Pretrivialization.linearEquivAt

added theorem Bundle.Pretrivialization.linearMapAt_apply

added theorem Bundle.Pretrivialization.linearMapAt_def_of_mem

added theorem Bundle.Pretrivialization.linearMapAt_def_of_notMem

added theorem Bundle.Pretrivialization.linearMapAt_eq_zero

added theorem Bundle.Pretrivialization.linearMapAt_symmₗ

added theorem Bundle.Pretrivialization.symmₗ_linearMapAt

deleted def Bundle.zeroSection

deleted theorem Bundle.zeroSection_proj

deleted theorem Bundle.zeroSection_snd

deleted def ContinuousLinearMap.inCoordinates

deleted theorem ContinuousLinearMap.inCoordinates_eq

deleted theorem Pretrivialization.coe_linearMapAt

deleted theorem Pretrivialization.coe_linearMapAt_of_mem

deleted theorem Pretrivialization.linear

deleted def Pretrivialization.linearEquivAt

deleted theorem Pretrivialization.linearMapAt_apply

deleted theorem Pretrivialization.linearMapAt_def_of_mem

deleted theorem Pretrivialization.linearMapAt_def_of_notMem

deleted theorem Pretrivialization.linearMapAt_eq_zero

deleted theorem Pretrivialization.linearMapAt_symmₗ

deleted theorem Pretrivialization.symmₗ_linearMapAt

deleted theorem Trivialization.apply_eq_prod_continuousLinearEquivAt

deleted theorem Trivialization.apply_symm_apply_eq_coordChangeL

deleted theorem Trivialization.coe_continuousLinearEquivAt_eq

deleted theorem Trivialization.coe_coordChangeL'

deleted theorem Trivialization.coe_coordChangeL

deleted theorem Trivialization.coe_linearMapAt

deleted theorem Trivialization.coe_linearMapAt_of_mem

deleted theorem Trivialization.coe_symmₗ

deleted theorem Trivialization.comp_continuousLinearEquivAt_eq_coord_change

deleted def Trivialization.continuousLinearEquivAt

deleted theorem Trivialization.continuousLinearEquivAt_apply'

deleted def Trivialization.continuousLinearMapAt

deleted theorem Trivialization.continuousLinearMapAt_symmL

deleted def Trivialization.coordChangeL

deleted theorem Trivialization.coordChangeL_apply'

deleted theorem Trivialization.coordChangeL_apply

deleted theorem Trivialization.coordChangeL_symm_apply

deleted def Trivialization.linearEquivAt

deleted theorem Trivialization.linearEquivAt_apply

deleted theorem Trivialization.linearEquivAt_symm_apply

deleted theorem Trivialization.linearMapAt_apply

deleted theorem Trivialization.linearMapAt_def_of_mem

deleted theorem Trivialization.linearMapAt_def_of_notMem

deleted theorem Trivialization.linearMapAt_symmₗ

deleted theorem Trivialization.mk_coordChangeL

deleted def Trivialization.symmL

deleted theorem Trivialization.symmL_continuousLinearMapAt

deleted theorem Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm

deleted theorem Trivialization.symm_continuousLinearEquivAt_eq

deleted theorem Trivialization.symm_coordChangeL

deleted theorem Trivialization.symmₗ_linearMapAt

deleted def VectorBundleCore.Base

deleted def VectorBundleCore.Fiber

deleted def VectorBundleCore.Index

deleted theorem VectorBundleCore.baseSet_at

deleted theorem VectorBundleCore.coe_coordChange

deleted theorem VectorBundleCore.continuous_proj

deleted theorem VectorBundleCore.coordChange_linear_comp

deleted theorem VectorBundleCore.isOpenMap_proj

deleted def VectorBundleCore.localTriv

deleted def VectorBundleCore.localTrivAt

deleted theorem VectorBundleCore.localTrivAt_apply

deleted theorem VectorBundleCore.localTrivAt_apply_mk

deleted theorem VectorBundleCore.localTrivAt_def

deleted theorem VectorBundleCore.localTriv_apply

deleted theorem VectorBundleCore.localTriv_continuousLinearMapAt

deleted theorem VectorBundleCore.localTriv_coordChange_eq

deleted theorem VectorBundleCore.localTriv_symmL

deleted theorem VectorBundleCore.localTriv_symm_apply

deleted theorem VectorBundleCore.localTriv_symm_fst

deleted theorem VectorBundleCore.mem_localTrivAt_baseSet

deleted theorem VectorBundleCore.mem_localTriv_source

deleted theorem VectorBundleCore.mem_localTriv_target

deleted theorem VectorBundleCore.mem_source_at

deleted theorem VectorBundleCore.mem_trivChange_source

deleted def VectorBundleCore.toFiberBundleCore

deleted def VectorBundleCore.trivChange

deleted theorem VectorBundleCore.trivializationAt_continuousLinearMapAt

deleted theorem VectorBundleCore.trivializationAt_coordChange_eq

deleted theorem VectorBundleCore.trivializationAt_symmL

deleted structure VectorBundleCore

deleted theorem VectorPrebundle.continuousOn_coordChange

deleted theorem VectorPrebundle.continuous_totalSpaceMk

deleted def VectorPrebundle.coordChange

deleted theorem VectorPrebundle.coordChange_apply

deleted theorem VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas

deleted theorem VectorPrebundle.mem_trivialization_at_source

deleted theorem VectorPrebundle.mk_coordChange

deleted def VectorPrebundle.toFiberBundle

deleted def VectorPrebundle.toFiberPrebundle

deleted theorem VectorPrebundle.toVectorBundle

deleted theorem VectorPrebundle.totalSpaceMk_preimage_source

deleted def VectorPrebundle.totalSpaceTopology

deleted def VectorPrebundle.trivializationOfMemPretrivializationAtlas

deleted structure VectorPrebundle

deleted theorem continuousOn_coordChange

deleted def trivialVectorBundleCore

Modified Mathlib/Topology/VectorBundle/Constructions.lean

added theorem Bundle.Trivialization.continuousLinearEquivAt_prod

added theorem Bundle.Trivialization.coordChangeL_prod

added theorem Bundle.Trivialization.prod_apply'

deleted theorem Trivialization.continuousLinearEquivAt_prod

deleted theorem Trivialization.coordChangeL_prod

deleted theorem Trivialization.prod_apply'

Modified Mathlib/Topology/VectorBundle/Hom.lean

added def Bundle.Pretrivialization.continuousLinearMap

added def Bundle.Pretrivialization.continuousLinearMapCoordChange

added theorem Bundle.Pretrivialization.continuousLinearMapCoordChange_apply

added theorem Bundle.Pretrivialization.continuousLinearMap_apply

added theorem Bundle.Pretrivialization.continuousLinearMap_symm_apply'

added theorem Bundle.Pretrivialization.continuousLinearMap_symm_apply

added theorem Bundle.Pretrivialization.continuousOn_continuousLinearMapCoordChange

added theorem Bundle.Trivialization.baseSet_continuousLinearMap

added def Bundle.Trivialization.continuousLinearMap

added theorem Bundle.Trivialization.continuousLinearMap_apply

deleted def Pretrivialization.continuousLinearMap

deleted def Pretrivialization.continuousLinearMapCoordChange

deleted theorem Pretrivialization.continuousLinearMapCoordChange_apply

deleted theorem Pretrivialization.continuousLinearMap_apply

deleted theorem Pretrivialization.continuousLinearMap_symm_apply'

deleted theorem Pretrivialization.continuousLinearMap_symm_apply

deleted theorem Pretrivialization.continuousOn_continuousLinearMapCoordChange

deleted theorem Trivialization.baseSet_continuousLinearMap

deleted def Trivialization.continuousLinearMap

deleted theorem Trivialization.continuousLinearMap_apply