Commit 2023-05-22 16:36 2acd194d

View on Github →

feat: port Topology.VectorBundle.Basic (#4187)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/VectorBundle/Basic.lean

added def Bundle.zeroSection

added theorem Bundle.zeroSection_proj

added theorem Bundle.zeroSection_snd

added def ContinuousLinearMap.inCoordinates

added theorem ContinuousLinearMap.inCoordinates_eq

added theorem Pretrivialization.coe_linearMapAt

added theorem Pretrivialization.coe_linearMapAt_of_mem

added theorem Pretrivialization.linear

added def Pretrivialization.linearEquivAt

added theorem Pretrivialization.linearMapAt_apply

added theorem Pretrivialization.linearMapAt_def_of_mem

added theorem Pretrivialization.linearMapAt_def_of_not_mem

added theorem Pretrivialization.linearMapAt_eq_zero

added theorem Pretrivialization.linearMapAt_symmₗ

added theorem Pretrivialization.symmₗ_linearMapAt

added theorem Trivialization.apply_eq_prod_continuousLinearEquivAt

added theorem Trivialization.apply_symm_apply_eq_coordChangeL

added theorem Trivialization.coe_continuousLinearEquivAt_eq

added theorem Trivialization.coe_coordChangeL'

added theorem Trivialization.coe_coordChangeL

added theorem Trivialization.coe_linearMapAt

added theorem Trivialization.coe_linearMapAt_of_mem

added theorem Trivialization.coe_symmₗ

added theorem Trivialization.comp_continuousLinearEquivAt_eq_coord_change

added def Trivialization.continuousLinearEquivAt

added theorem Trivialization.continuousLinearEquivAt_apply'

added def Trivialization.continuousLinearMapAt

added theorem Trivialization.continuousLinearMapAt_symmL

added def Trivialization.coordChangeL

added theorem Trivialization.coordChangeL_apply'

added theorem Trivialization.coordChangeL_apply

added theorem Trivialization.coordChangeL_symm_apply

added def Trivialization.linearEquivAt

added theorem Trivialization.linearEquivAt_apply

added theorem Trivialization.linearEquivAt_symm_apply

added theorem Trivialization.linearMapAt_apply

added theorem Trivialization.linearMapAt_def_of_mem

added theorem Trivialization.linearMapAt_def_of_not_mem

added theorem Trivialization.linearMapAt_symmₗ

added theorem Trivialization.mk_coordChangeL

added def Trivialization.symmL

added theorem Trivialization.symmL_continuousLinearMapAt

added theorem Trivialization.symm_apply_eq_mk_continuousLinearEquivAt_symm

added theorem Trivialization.symm_continuousLinearEquivAt_eq

added theorem Trivialization.symm_coordChangeL

added theorem Trivialization.symmₗ_linearMapAt

added def VectorBundleCore.Base

added def VectorBundleCore.Fiber

added def VectorBundleCore.Index

added theorem VectorBundleCore.baseSet_at

added theorem VectorBundleCore.coe_coordChange

added theorem VectorBundleCore.continuous_proj

added theorem VectorBundleCore.coordChange_linear_comp

added theorem VectorBundleCore.isOpenMap_proj

added def VectorBundleCore.localTriv

added def VectorBundleCore.localTrivAt

added theorem VectorBundleCore.localTrivAt_apply

added theorem VectorBundleCore.localTrivAt_apply_mk

added theorem VectorBundleCore.localTrivAt_def

added theorem VectorBundleCore.localTriv_apply

added theorem VectorBundleCore.localTriv_continuousLinearMapAt

added theorem VectorBundleCore.localTriv_coordChange_eq

added theorem VectorBundleCore.localTriv_symmL

added theorem VectorBundleCore.localTriv_symm_apply

added theorem VectorBundleCore.localTriv_symm_fst

added theorem VectorBundleCore.mem_localTrivAt_baseSet

added theorem VectorBundleCore.mem_localTriv_source

added theorem VectorBundleCore.mem_localTriv_target

added theorem VectorBundleCore.mem_source_at

added theorem VectorBundleCore.mem_trivChange_source

added def VectorBundleCore.toFiberBundleCore

added def VectorBundleCore.trivChange

added theorem VectorBundleCore.trivializationAt_continuousLinearMapAt

added theorem VectorBundleCore.trivializationAt_coordChange_eq

added theorem VectorBundleCore.trivializationAt_symmL

added structure VectorBundleCore

added theorem VectorPrebundle.continuousOn_coordChange

added theorem VectorPrebundle.continuous_totalSpaceMk

added def VectorPrebundle.coordChange

added theorem VectorPrebundle.coordChange_apply

added def VectorPrebundle.fiberTopology

added theorem VectorPrebundle.inducing_totalSpaceMk

added theorem VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas

added theorem VectorPrebundle.mem_trivialization_at_source

added theorem VectorPrebundle.mk_coordChange

added def VectorPrebundle.toFiberBundle

added def VectorPrebundle.toFiberPrebundle

added theorem VectorPrebundle.to_vectorBundle

added theorem VectorPrebundle.totalSpaceMk_preimage_source

added def VectorPrebundle.totalSpaceTopology

added def VectorPrebundle.trivializationOfMemPretrivializationAtlas

added structure VectorPrebundle

added theorem continuousOn_coordChange

added def trivialVectorBundleCore