Commit 2023-07-06 06:47 5edb251a

View on Github →

refactor: redefine Bundle.TotalSpace (#5720) Forward-port leanprover-community/mathlib#19221

Estimated changes

Modified Mathlib/Data/Bundle.lean

modified def Bundle.Pullback.lift

deleted theorem Bundle.Pullback.proj_lift

modified def Bundle.Pullback

modified theorem Bundle.TotalSpace.eta

added theorem Bundle.TotalSpace.exists

added theorem Bundle.TotalSpace.mk_inj

added theorem Bundle.TotalSpace.mk_injective

deleted def Bundle.TotalSpace.proj

deleted theorem Bundle.TotalSpace.proj_mk

added theorem Bundle.TotalSpace.range_mk

added def Bundle.TotalSpace.toProd

added def Bundle.TotalSpace.trivialSnd

added structure Bundle.TotalSpace

deleted def Bundle.TotalSpace

deleted def Bundle.Trivial.projSnd

modified def Bundle.Trivial

deleted theorem Bundle.coe_fst

deleted theorem Bundle.coe_snd

deleted theorem Bundle.coe_snd_map_apply

deleted theorem Bundle.coe_snd_map_smul

modified def Bundle.pullbackTotalSpaceEmbedding

deleted theorem Bundle.pullbackTotalSpaceEmbedding_snd

deleted theorem Bundle.sigma_mk_eq_totalSpaceMk

deleted def Bundle.totalSpaceMk

Modified Mathlib/Geometry/Manifold/MFDeriv.lean

modified theorem Trivialization.mdifferentiable

modified theorem UniqueMDiffWithinAt.smooth_bundle_preimage

deleted theorem tangentMapWithin_fst

deleted theorem tangentMap_fst

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

modified theorem Bundle.contMDiffAt_proj

modified theorem Bundle.contMDiffAt_totalSpace

modified theorem Bundle.contMDiffOn_proj

modified theorem Bundle.contMDiffWithinAt_proj

modified theorem Bundle.contMDiffWithinAt_totalSpace

modified theorem Bundle.contMDiff_proj

modified theorem Bundle.smoothAt_proj

modified theorem Bundle.smoothOn_proj

modified theorem Bundle.smoothWithinAt_proj

modified theorem Bundle.smooth_proj

modified theorem Bundle.smooth_zeroSection

modified theorem ContMDiffWithinAt.change_section_trivialization

modified theorem FiberBundle.chartedSpace'_chartAt

modified theorem FiberBundle.chartedSpace_chartAt

modified theorem FiberBundle.chartedSpace_chartAt_symm_fst

modified theorem Trivialization.contMDiffAt_iff

modified theorem Trivialization.contMDiffOn_iff

modified theorem Trivialization.contMDiffWithinAt_iff

modified theorem Trivialization.contMDiffWithinAt_snd_comp_iff₂

modified theorem Trivialization.contMDiff_iff

modified theorem Trivialization.smoothAt_iff

modified theorem Trivialization.smoothOn

modified theorem Trivialization.smoothOn_iff

modified theorem Trivialization.smoothOn_symm

modified theorem Trivialization.smoothWithinAt_iff

modified theorem Trivialization.smooth_iff

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

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

Modified Mathlib/Topology/Covering.lean

Modified Mathlib/Topology/FiberBundle/Basic.lean

modified theorem FiberBundle.continuousAt_totalSpace

modified theorem FiberBundle.continuousWithinAt_totalSpace

modified theorem FiberBundle.continuous_proj

modified theorem FiberBundle.continuous_totalSpaceMk

modified theorem FiberBundle.isOpenMap_proj

modified theorem FiberBundle.map_proj_nhds

modified theorem FiberBundle.mem_trivializationAt_proj_source

modified theorem FiberBundle.quotientMap_proj

modified theorem FiberBundle.surjective_proj

modified theorem FiberBundle.totalSpaceMk_closedEmbedding

modified theorem FiberBundle.totalSpaceMk_embedding

modified theorem FiberBundle.totalSpaceMk_inducing

modified theorem FiberBundle.trivializationAt_proj_fst

modified def FiberBundleCore.TotalSpace

modified def FiberBundleCore.localTrivAt

deleted theorem FiberBundleCore.mem_source_at

added theorem FiberBundleCore.mk_mem_localTrivAt_source

modified theorem FiberPrebundle.continuousOn_of_comp_right

modified theorem FiberPrebundle.continuous_proj

modified theorem FiberPrebundle.isOpen_source

modified theorem FiberPrebundle.isOpen_target_of_mem_pretrivializationAtlas_inter

modified def FiberPrebundle.totalSpaceTopology

Modified Mathlib/Topology/FiberBundle/Constructions.lean

modified theorem Bundle.Trivial.eq_trivialization

added def Bundle.Trivial.homeomorphProd

added theorem Bundle.Trivial.inducing_toProd

modified def Bundle.Trivial.trivialization

modified theorem Pullback.continuous_lift

modified theorem Pullback.continuous_proj

modified theorem Trivialization.Prod.left_inv

modified def Trivialization.Prod.toFun'

Modified Mathlib/Topology/FiberBundle/Trivialization.lean

modified theorem Pretrivialization.apply_mk_symm

modified theorem Pretrivialization.coe_symm_of_not_mem

modified theorem Pretrivialization.mk_symm

modified theorem Pretrivialization.symm_apply

modified theorem Pretrivialization.symm_apply_apply_mk

modified theorem Pretrivialization.symm_apply_of_not_mem

modified theorem Pretrivialization.symm_coe_proj

modified theorem Pretrivialization.symm_proj_apply

modified theorem Trivialization.apply_mk_symm

modified theorem Trivialization.continuousOn_symm

modified theorem Trivialization.mk_symm

modified theorem Trivialization.symm_apply

modified theorem Trivialization.symm_apply_apply

modified theorem Trivialization.symm_apply_apply_mk

modified theorem Trivialization.symm_apply_of_not_mem

modified theorem Trivialization.symm_coe_proj

modified theorem Trivialization.symm_proj_apply

Modified Mathlib/Topology/VectorBundle/Basic.lean

modified def Bundle.zeroSection

modified theorem Bundle.zeroSection_proj

modified theorem Bundle.zeroSection_snd

modified theorem Pretrivialization.coe_linearMapAt

modified theorem Pretrivialization.coe_linearMapAt_of_mem

modified def Pretrivialization.linearEquivAt

modified theorem Pretrivialization.linearMapAt_apply

modified theorem Pretrivialization.linearMapAt_def_of_mem

modified theorem Pretrivialization.linearMapAt_def_of_not_mem

modified theorem Pretrivialization.linearMapAt_eq_zero

modified theorem Pretrivialization.linearMapAt_symmₗ

modified theorem Pretrivialization.symmₗ_linearMapAt

modified theorem Trivialization.apply_eq_prod_continuousLinearEquivAt

modified theorem Trivialization.apply_symm_apply_eq_coordChangeL

modified theorem Trivialization.coe_continuousLinearEquivAt_eq

modified theorem Trivialization.coe_coordChangeL'

modified theorem Trivialization.coe_coordChangeL

modified theorem Trivialization.coe_linearMapAt

modified theorem Trivialization.coe_linearMapAt_of_mem

modified theorem Trivialization.coe_symmₗ

modified theorem Trivialization.comp_continuousLinearEquivAt_eq_coord_change

modified def Trivialization.continuousLinearEquivAt

modified theorem Trivialization.continuousLinearEquivAt_apply'

modified def Trivialization.continuousLinearMapAt

modified theorem Trivialization.continuousLinearMapAt_symmL

modified def Trivialization.coordChangeL

modified theorem Trivialization.coordChangeL_apply'

modified theorem Trivialization.coordChangeL_apply

modified theorem Trivialization.coordChangeL_symm_apply

modified def Trivialization.linearEquivAt

modified theorem Trivialization.linearEquivAt_apply

modified theorem Trivialization.linearEquivAt_symm_apply

modified theorem Trivialization.linearMapAt_apply

modified theorem Trivialization.linearMapAt_def_of_mem

modified theorem Trivialization.linearMapAt_def_of_not_mem

modified theorem Trivialization.linearMapAt_symmₗ

modified theorem Trivialization.mk_coordChangeL

modified def Trivialization.symmL

modified theorem Trivialization.symmL_continuousLinearMapAt

modified theorem Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm

modified theorem Trivialization.symm_continuousLinearEquivAt_eq

modified theorem Trivialization.symm_coordChangeL

modified theorem Trivialization.symmₗ_linearMapAt

modified def VectorBundleCore.localTriv

modified def VectorBundleCore.localTrivAt

modified theorem VectorPrebundle.continuousOn_coordChange

modified def VectorPrebundle.coordChange

modified theorem VectorPrebundle.coordChange_apply

modified theorem VectorPrebundle.mk_coordChange

modified def VectorPrebundle.totalSpaceTopology

modified theorem continuousOn_coordChange

Modified Mathlib/Topology/VectorBundle/Constructions.lean

modified theorem Trivialization.continuousLinearEquivAt_prod