Basic

📁 Source: Mathlib/Topology/VectorBundle/Basic.lean

Statistics

Metric	Count
Definitions zeroSection, inCoordinates, IsLinear, linearEquivAt, linearMapAt, symmₗ, IsLinear, continuousLinearEquivAt, continuousLinearMapAt, coordChangeL, linearEquivAt, linearMapAt, symmL, symmₗ, VectorBundle, VectorBundleCore, TotalSpace, addCommGroupFiber, baseSet, coordChange, fiberBundle, indexAt, localTriv, localTrivAt, moduleFiber, proj, toFiberBundleCore, toTopologicalSpace, topologicalSpaceFiber, trivChange, VectorPrebundle, coordChange, pretrivializationAt, pretrivializationAtlas, toFiberBundle, toFiberPrebundle, totalSpaceTopology, trivializationOfMemPretrivializationAtlas, instInhabitedVectorBundleCore, trivialVectorBundleCore	40
Theorems zeroSection_proj, zeroSection_snd, inCoordinates_eq, linear, coe_linearMapAt, coe_linearMapAt_of_mem, linear, linearEquivAt_apply, linearEquivAt_symm_apply, linearMapAt_apply, linearMapAt_def_of_mem, linearMapAt_def_of_notMem, linearMapAt_eq_zero, linearMapAt_symmₗ, symmₗ_apply, symmₗ_linearMapAt, linear, apply_eq_prod_continuousLinearEquivAt, apply_symm_apply_eq_coordChangeL, coe_continuousLinearEquivAt_eq, coe_coordChangeL, coe_coordChangeL', coe_linearMapAt, coe_linearMapAt_of_mem, coe_symmₗ, comp_continuousLinearEquivAt_eq_coord_change, continuousLinearEquivAt_apply, continuousLinearEquivAt_apply', continuousLinearEquivAt_symm_apply, continuousLinearMapAt_apply, continuousLinearMapAt_symmL, coordChangeL_apply, coordChangeL_apply', coordChangeL_symm_apply, linear, linearEquivAt_apply, linearEquivAt_symm_apply, linearMapAt_apply, linearMapAt_def_of_mem, linearMapAt_def_of_notMem, linearMapAt_symmₗ, mk_coordChangeL, symmL_apply, symmL_continuousLinearMapAt, symm_apply_eq_mk_continuousLinearEquivAt_symm, symm_continuousLinearEquivAt_eq, symm_coordChangeL, symmₗ_linearMapAt, isLinear, zeroSection, continuousOn_coordChange', trivialization_linear', baseSet_at, coe_coordChange, continuousOn_coordChange, continuous_proj, coordChange_comp, coordChange_linear_comp, coordChange_self, inCoordinates_eq, isOpenMap_proj, isOpen_baseSet, isLinear, localTrivAt_apply, localTrivAt_apply_mk, localTrivAt_def, localTriv_apply, localTriv_continuousLinearMapAt, localTriv_coordChange_eq, localTriv_symmL, localTriv_symm_apply, localTriv_symm_fst, mem_baseSet_at, mem_localTrivAt_baseSet, mem_localTriv_source, mem_localTriv_target, mem_source_at, mem_trivChange_source, toFiberBundleCore_baseSet, toFiberBundleCore_coordChange, toFiberBundleCore_indexAt, trivializationAt, trivializationAt_continuousLinearMapAt, trivializationAt_coordChange_eq, trivializationAt_symmL, vectorBundle, continuousOn_coordChange, continuous_totalSpaceMk, coordChange_apply, exists_coordChange, linear_trivializationOfMemPretrivializationAtlas, mem_base_pretrivializationAt, mem_trivialization_at_source, mk_coordChange, pretrivialization_linear', pretrivialization_mem_atlas, toVectorBundle, totalSpaceMk_isInducing, totalSpaceMk_preimage_source, continuousOn_coordChange, trivialization_linear	101
Total	141

Bundle

Definitions

Name	Category	Theorems
zeroSection 📖	CompOp	12 math math: TangentBundle.tangentMap_tangentBundle_pure, contMDiffOn_zeroSection, contMDiffWithinAt_zeroSection, zeroSection_proj, Trivialization.zeroSection, zeroSection_snd, contMDiffAt_zeroSection, mdifferentiableWithinAt_zeroSection, contMDiff_zeroSection, mdifferentiableOn_zeroSection, mdifferentiable_zeroSection, mdifferentiableAt_zeroSection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
zeroSection_proj 📖	mathematical	—	TotalSpace.proj zeroSection	—	—
zeroSection_snd 📖	mathematical	—	TotalSpace.snd zeroSection TotalSpace.proj	—	—

ContinuousLinearMap

Definitions

Name	Category	Theorems
inCoordinates 📖	CompOp	12 math math: inCoordinates_apply_eq₂, mdifferentiableAt_hom_bundle, contMDiffAt_hom_bundle, inCoordinates_eq, VectorBundleCore.inCoordinates_eq, continuousAt_hom_bundle, continuousWithinAt_hom_bundle, hom_chart, hom_trivializationAt_apply, mdifferentiableWithinAt_hom_bundle, inCoordinates_tangent_bundle_core_model_space, contMDiffWithinAt_hom_bundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inCoordinates_eq 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj FiberBundle.trivializationAt	inCoordinates comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule RingHomCompTriple.right_ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.continuousLinearEquivAt trivialization_linear instMemTrivializationAtlasTrivializationAt RingHomCompTriple.ids ContinuousLinearEquiv.symm	—	ext RingHomCompTriple.right_ids RingHomInvPair.ids trivialization_linear instMemTrivializationAtlasTrivializationAt RingHomCompTriple.ids Trivialization.coe_continuousLinearEquivAt_eq

Pretrivialization

Definitions

Name	Category	Theorems
IsLinear 📖	CompData	3 math math: Trivialization.toPretrivialization.isLinear, VectorPrebundle.pretrivialization_linear', continuousLinearMap.isLinear
linearEquivAt 📖	CompOp	3 math math: linearEquivAt_symm_apply, linearMapAt_def_of_mem, linearEquivAt_apply
linearMapAt 📖	CompOp	8 math math: linearMapAt_def_of_notMem, linearMapAt_eq_zero, coe_linearMapAt, linearMapAt_apply, linearMapAt_symmₗ, linearMapAt_def_of_mem, symmₗ_linearMapAt, coe_linearMapAt_of_mem
symmₗ 📖	CompOp	3 math math: linearMapAt_symmₗ, symmₗ_apply, symmₗ_linearMapAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_linearMapAt 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj toFun' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids linearMapAt.eq_1
coe_linearMapAt_of_mem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt toFun'	—	coe_linearMapAt
linear 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	IsLinearMap toFun'	—	IsLinear.linear
linearEquivAt_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike linearEquivAt toFun'	—	RingHomInvPair.ids
linearEquivAt_symm_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm linearEquivAt symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
linearMapAt_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj toFun' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	coe_linearMapAt
linearMapAt_def_of_mem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	linearMapAt LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids linearEquivAt	—	RingHomInvPair.ids
linearMapAt_def_of_notMem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	linearMapAt LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instZero	—	RingHomInvPair.ids
linearMapAt_eq_zero 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	linearMapAt LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instZero	—	RingHomInvPair.ids
linearMapAt_symmₗ 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt symmₗ	—	RingHomInvPair.ids linearMapAt_def_of_mem LinearEquiv.right_inv
symmₗ_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike symmₗ symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
symmₗ_linearMapAt 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike symmₗ linearMapAt	—	RingHomInvPair.ids linearMapAt_def_of_mem LinearEquiv.left_inv

Pretrivialization.IsLinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linear 📖	mathematical	Set Set.instMembership Pretrivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	IsLinearMap Pretrivialization.toFun'	—	—

Trivialization

Definitions

Name	Category	Theorems
IsLinear 📖	CompData	7 math math: pullback_linear, trivialization_linear, VectorBundle.trivialization_linear', VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas, prod.isLinear, Bundle.Trivial.trivialization.isLinear, VectorBundleCore.localTriv.isLinear
continuousLinearEquivAt 📖	CompOp	12 math math: Bundle.Trivial.continuousLinearEquivAt_trivialization, continuousLinearEquivAt_apply, comp_continuousLinearEquivAt_eq_coord_change, symm_apply_eq_mk_continuousLinearEquivAt_symm, continuousLinearEquivAt_apply', apply_eq_prod_continuousLinearEquivAt, continuousLinearEquivAt_prod, coe_continuousLinearEquivAt_eq, continuousLinearEquivAt_symm_apply, ContinuousLinearMap.inCoordinates_eq, symm_continuousLinearEquivAt_eq, prod_apply'
continuousLinearMapAt 📖	CompOp	17 math math: TangentBundle.continuousLinearMapAt_model_space, continuousLinearMapAt_apply, Pretrivialization.continuousLinearMap_symm_apply', VectorBundleCore.localTriv_continuousLinearMapAt, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, Bundle.Trivial.continuousLinearMapAt_trivialization, VectorBundleCore.trivializationAt_continuousLinearMapAt, symmL_continuousLinearMapAt, eventually_norm_symmL_trivializationAt_self_comp_lt, continuousLinearMap_apply, TangentBundle.continuousLinearMapAt_trivializationAt, eventually_norm_symmL_trivializationAt_comp_self_lt, coe_continuousLinearEquivAt_eq, Pretrivialization.continuousLinearMap_apply, continuousLinearMapAt_symmL, Pretrivialization.continuousLinearMap_symm_apply, eventually_norm_trivializationAt_lt
coordChangeL 📖	CompOp	30 math math: ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, mdifferentiableOn_symm_coordChangeL, comp_continuousLinearEquivAt_eq_coord_change, VectorBundleCore.trivializationAt_coordChange_eq, ContMDiffOn.coordChangeL, MDifferentiableOn.coordChangeL, contMDiffAt_coordChangeL, MDifferentiableWithinAt.coordChangeL, VectorBundle.continuousOn_coordChange', contMDiffOn_symm_coordChangeL, symm_coordChangeL, VectorBundleCore.localTriv_coordChange_eq, coordChangeL_symm_apply, mk_coordChangeL, coe_coordChangeL', mdifferentiableOn_coordChangeL, coordChangeL_apply, ContMDiffVectorBundle.contMDiffOn_coordChangeL, MDifferentiableAt.coordChangeL, coe_coordChangeL, ContMDiffWithinAt.coordChangeL, Bundle.Trivial.trivialization.coordChangeL, mdifferentiableAt_coordChangeL, apply_symm_apply_eq_coordChangeL, contMDiffOn_coordChangeL, continuousOn_coordChange, coordChangeL_apply', ContMDiff.coordChangeL, coordChangeL_prod
linearEquivAt 📖	CompOp	6 math math: linearEquivAt_apply, coordChangeL_symm_apply, coe_coordChangeL', linearMapAt_def_of_mem, coe_coordChangeL, linearEquivAt_symm_apply
linearMapAt 📖	CompOp	10 math math: continuousLinearMapAt_apply, linearMapAt_symmₗ, Bundle.Trivial.linearMapAt_trivialization, inCoordinates_apply_eq₂, coe_linearMapAt, symmₗ_linearMapAt, coe_linearMapAt_of_mem, linearMapAt_def_of_mem, linearMapAt_def_of_notMem, linearMapAt_apply
symmL 📖	CompOp	17 math math: Bundle.Trivial.symmL_trivialization, VectorBundleCore.trivializationAt_symmL, TangentBundle.symmL_trivializationAt, Pretrivialization.continuousLinearMap_symm_apply', VectorBundleCore.localTriv_symmL, TangentBundle.symmL_trivializationAt_eq_core, symmL_continuousLinearMapAt, eventually_norm_symmL_trivializationAt_self_comp_lt, continuousLinearMap_apply, eventually_norm_symmL_trivializationAt_comp_self_lt, eventually_norm_symmL_trivializationAt_lt, TangentBundle.symmL_model_space, Pretrivialization.continuousLinearMap_apply, symm_continuousLinearEquivAt_eq, continuousLinearMapAt_symmL, Pretrivialization.continuousLinearMap_symm_apply, symmL_apply
symmₗ 📖	CompOp	4 math math: linearMapAt_symmₗ, coe_symmₗ, symmₗ_linearMapAt, Bundle.Trivial.symmₗ_trivialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_eq_prod_continuousLinearEquivAt 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	toFun' DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt	—	RingHomInvPair.ids coe_fst source_eq
apply_symm_apply_eq_coordChangeL 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	toFun' OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike coordChangeL	—	RingHomInvPair.ids mk_coordChangeL mk_symm
coe_continuousLinearEquivAt_eq 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt ContinuousLinearMap ContinuousLinearMap.funLike continuousLinearMapAt	—	coe_linearMapAt_of_mem
coe_coordChangeL 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike coordChangeL LinearEquiv DFinsupp.instEquivLikeLinearEquiv LinearEquiv.trans RingHomCompTriple.ids LinearEquiv.symm linearEquivAt	—	RingHomInvPair.ids RingHomCompTriple.ids
coe_coordChangeL' 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	ContinuousLinearEquiv.toLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids coordChangeL LinearEquiv.trans RingHomCompTriple.ids LinearEquiv.symm linearEquivAt	—	LinearEquiv.coe_injective RingHomInvPair.ids RingHomCompTriple.ids coe_coordChangeL
coe_linearMapAt 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj toFun' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Pretrivialization.coe_linearMapAt toPretrivialization.isLinear
coe_linearMapAt_of_mem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt toFun'	—	coe_linearMapAt
coe_symmₗ 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike symmₗ symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
comp_continuousLinearEquivAt_eq_coord_change 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContinuousLinearEquiv.trans DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids RingHomCompTriple.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearEquiv.symm continuousLinearEquivAt coordChangeL	—	ContinuousLinearEquiv.ext RingHomInvPair.ids RingHomCompTriple.ids coordChangeL_apply
continuousLinearEquivAt_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt toFun'	—	RingHomInvPair.ids
continuousLinearEquivAt_apply' 📖	mathematical	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt baseSet mem_source Bundle.TotalSpace.snd toFun'	—	RingHomInvPair.ids mem_source
continuousLinearEquivAt_symm_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquivAt symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
continuousLinearMapAt_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike continuousLinearMapAt LinearMap LinearMap.instFunLike linearMapAt	—	—
continuousLinearMapAt_symmL 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike continuousLinearMapAt symmL	—	linearMapAt_symmₗ
coordChangeL_apply 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike coordChangeL toFun' symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids RingHomCompTriple.ids coe_coordChangeL
coordChangeL_apply' 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike coordChangeL toFun' OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph	—	RingHomInvPair.ids coordChangeL_apply mk_symm
coordChangeL_symm_apply 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm coordChangeL LinearEquiv DFinsupp.instEquivLikeLinearEquiv LinearEquiv.trans RingHomCompTriple.ids LinearEquiv.symm linearEquivAt	—	RingHomInvPair.ids
linear 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	IsLinearMap toFun'	—	IsLinear.linear
linearEquivAt_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv linearEquivAt toFun'	—	RingHomInvPair.ids
linearEquivAt_symm_apply 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm linearEquivAt symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
linearMapAt_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj toFun' AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	coe_linearMapAt
linearMapAt_def_of_mem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	linearMapAt LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids linearEquivAt	—	RingHomInvPair.ids toPretrivialization.isLinear
linearMapAt_def_of_notMem 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	linearMapAt LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instZero	—	RingHomInvPair.ids toPretrivialization.isLinear
linearMapAt_symmₗ 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt symmₗ	—	Pretrivialization.linearMapAt_symmₗ toPretrivialization.isLinear
mk_coordChangeL 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike coordChangeL toFun' symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids mk_symm coe_fst' proj_symm_apply' coordChangeL_apply
symmL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike symmL symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
symmL_continuousLinearMapAt 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike symmL continuousLinearMapAt	—	symmₗ_linearMapAt
symm_apply_eq_mk_continuousLinearEquivAt_symm 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	OpenPartialHomeomorph.toFun' instTopologicalSpaceProd OpenPartialHomeomorph.symm toOpenPartialHomeomorph DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquivAt	—	RingHomInvPair.ids mk_symm
symm_continuousLinearEquivAt_eq 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquivAt ContinuousLinearMap ContinuousLinearMap.funLike symmL	—	RingHomInvPair.ids
symm_coordChangeL 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	ContinuousLinearEquiv.symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids coordChangeL	—	ContinuousLinearEquiv.toLinearEquiv_injective RingHomInvPair.ids RingHomCompTriple.ids coe_coordChangeL' ContinuousLinearEquiv.toLinearEquiv_symm LinearEquiv.trans_symm LinearEquiv.symm_symm
symmₗ_linearMapAt 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike symmₗ linearMapAt	—	Pretrivialization.symmₗ_linearMapAt toPretrivialization.isLinear
zeroSection 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	toFun' Bundle.zeroSection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	RingHomInvPair.ids apply_eq_prod_continuousLinearEquivAt map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousSemilinearEquivClass.continuousSemilinearMapClass ContinuousLinearEquiv.continuousSemilinearEquivClass

Trivialization.IsLinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linear 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	IsLinearMap Trivialization.toFun'	—	—

Trivialization.toPretrivialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLinear 📖	mathematical	—	Pretrivialization.IsLinear Trivialization.toPretrivialization Bundle.TotalSpace Bundle.TotalSpace.proj	—	Trivialization.IsLinear.linear

VectorBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_coordChange' 📖	mathematical	—	ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear' Set Set.instInter Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	—
trivialization_linear' 📖	mathematical	—	Trivialization.IsLinear DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	—

VectorBundleCore

Definitions

Name	Category	Theorems
TotalSpace 📖	CompOp	1 math math: mem_localTriv_source
addCommGroupFiber 📖	CompOp	1 math math: localTriv_symm_apply
baseSet 📖	CompOp	10 math math: contMDiffOn_coordChange, isOpen_baseSet, baseSet_at, mem_trivChange_source, mem_baseSet_at, tangentBundleCore_baseSet, IsContMDiff.contMDiffOn_coordChange, continuousOn_coordChange, mem_localTriv_source, toFiberBundleCore_baseSet
coordChange 📖	CompOp	25 math math: toFiberBundleCore_coordChange, trivializationAt_symmL, coordChange_self, localTriv_continuousLinearMapAt, localTriv_symmL, TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, contMDiffOn_coordChange, localTriv_symm_fst, trivializationAt_coordChange_eq, localTriv_symm_apply, trivializationAt_continuousLinearMapAt, TangentBundle.coordChange_model_space, inTangentCoordinates_eq, coe_coordChange, tangentBundleCore_coordChange_model_space, localTriv_coordChange_eq, tangentBundleCore_coordChange, localTriv_apply, IsContMDiff.contMDiffOn_coordChange, inCoordinates_eq, continuousOn_coordChange, coordChange_linear_comp, coordChange_comp, tangentBundleCore_coordChange_achart
fiberBundle 📖	CompOp	6 math math: localTriv_continuousLinearMapAt, localTriv_symmL, instContMDiffVectorBundle, inCoordinates_eq, trivializationAt, vectorBundle
indexAt 📖	CompOp	12 math math: toFiberBundleCore_indexAt, trivializationAt_symmL, localTriv_continuousLinearMapAt, localTriv_symmL, localTriv_symm_fst, trivializationAt_coordChange_eq, localTriv_symm_apply, trivializationAt_continuousLinearMapAt, mem_baseSet_at, localTriv_apply, localTrivAt_def, tangentBundleCore_indexAt
localTriv 📖	CompOp	8 math math: mem_localTriv_target, localTriv_symm_fst, baseSet_at, localTriv_apply, localTrivAt_def, tangentBundleCore_localTriv_baseSet, mem_localTriv_source, localTriv.isLinear
localTrivAt 📖	CompOp	6 math math: localTrivAt_apply, mem_source_at, localTrivAt_def, localTrivAt_apply_mk, trivializationAt, mem_localTrivAt_baseSet
moduleFiber 📖	CompOp	10 math math: trivializationAt_symmL, localTriv_continuousLinearMapAt, localTriv_symmL, trivializationAt_coordChange_eq, trivializationAt_continuousLinearMapAt, instContMDiffVectorBundle, localTriv_coordChange_eq, inCoordinates_eq, localTriv.isLinear, vectorBundle
proj 📖	CompOp	2 math math: continuous_proj, isOpenMap_proj
toFiberBundleCore 📖	CompOp	7 math math: toFiberBundleCore_coordChange, toFiberBundleCore_indexAt, coe_coordChange, TangentBundle.chartAt, TangentBundle.trivializationAt_eq_localTriv, TangentBundle.chartAt_toPartialEquiv, toFiberBundleCore_baseSet
toTopologicalSpace 📖	CompOp	17 math math: mem_localTriv_target, continuous_proj, localTriv_symm_fst, localTrivAt_apply, isOpenMap_proj, baseSet_at, mem_source_at, instContMDiffVectorBundle, localTriv_apply, localTrivAt_apply_mk, tangentBundleCore_localTriv_baseSet, inCoordinates_eq, trivializationAt, mem_localTriv_source, localTriv.isLinear, mem_localTrivAt_baseSet, vectorBundle
topologicalSpaceFiber 📖	CompOp	8 math math: localTriv_continuousLinearMapAt, localTriv_symmL, instContMDiffVectorBundle, localTriv_coordChange_eq, inCoordinates_eq, trivializationAt, localTriv.isLinear, vectorBundle
trivChange 📖	CompOp	1 math math: mem_trivChange_source

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseSet_at 📖	mathematical	—	baseSet Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	—	—
coe_coordChange 📖	mathematical	—	FiberBundleCore.coordChange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFiberBundleCore DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange	—	—
continuousOn_coordChange 📖	mathematical	—	ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup coordChange Set Set.instInter baseSet	—	—
continuous_proj 📖	mathematical	—	Continuous Bundle.TotalSpace Fiber toTopologicalSpace proj	—	FiberBundleCore.continuous_proj
coordChange_comp 📖	mathematical	Set Set.instMembership Set.instInter baseSet	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange	—	—
coordChange_linear_comp 📖	mathematical	Set Set.instMembership Set.instInter baseSet	ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule RingHomCompTriple.ids coordChange	—	ContinuousLinearMap.ext RingHomCompTriple.ids coordChange_comp
coordChange_self 📖	mathematical	Set Set.instMembership baseSet	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange	—	—
inCoordinates_eq 📖	mathematical	Set Set.instMembership baseSet indexAt	ContinuousLinearMap.inCoordinates Fiber ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber toTopologicalSpace fiberBundle vectorBundle ContinuousLinearMap.comp DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule RingHomCompTriple.right_ids coordChange RingHomCompTriple.ids	—	vectorBundle RingHomCompTriple.right_ids RingHomCompTriple.ids ContinuousLinearMap.comp.congr_simp trivializationAt_continuousLinearMapAt trivializationAt_symmL
isOpenMap_proj 📖	mathematical	—	IsOpenMap Bundle.TotalSpace Fiber toTopologicalSpace proj	—	FiberBundleCore.isOpenMap_proj
isOpen_baseSet 📖	mathematical	—	IsOpen baseSet	—	—
localTrivAt_apply 📖	mathematical	—	Trivialization.toFun' Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj toTopologicalSpace localTrivAt Bundle.TotalSpace.snd	—	FiberBundleCore.localTrivAt_apply
localTrivAt_apply_mk 📖	mathematical	—	Trivialization.toFun' Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj toTopologicalSpace localTrivAt	—	localTrivAt_apply
localTrivAt_def 📖	mathematical	—	localTriv indexAt localTrivAt	—	—
localTriv_apply 📖	mathematical	—	Trivialization.toFun' Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj toTopologicalSpace localTriv DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange indexAt Bundle.TotalSpace.snd	—	—
localTriv_continuousLinearMapAt 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	Trivialization.continuousLinearMapAt ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber fiberBundle localTriv.isLinear coordChange indexAt	—	ContinuousLinearMap.ext localTriv.isLinear Trivialization.continuousLinearMapAt_apply Trivialization.coe_linearMapAt_of_mem
localTriv_coordChange_eq 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike Trivialization.coordChangeL topologicalSpaceFiber moduleFiber localTriv.isLinear ContinuousLinearMap ContinuousLinearMap.funLike coordChange	—	RingHomInvPair.ids localTriv.isLinear Trivialization.coordChangeL_apply' localTriv_symm_fst localTriv_apply coordChange_comp mem_baseSet_at
localTriv_symmL 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	Trivialization.symmL ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber fiberBundle localTriv.isLinear coordChange indexAt	—	ContinuousLinearMap.ext localTriv.isLinear Trivialization.symmL_apply Trivialization.symm_coe_proj Trivialization.symm_apply
localTriv_symm_apply 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	Trivialization.symm NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid addCommGroupFiber DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange indexAt	—	Trivialization.symm_apply
localTriv_symm_fst 📖	mathematical	—	OpenPartialHomeomorph.toFun' Bundle.TotalSpace Fiber instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace OpenPartialHomeomorph.symm Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTriv DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange indexAt	—	—
mem_baseSet_at 📖	mathematical	—	Set Set.instMembership baseSet indexAt	—	—
mem_localTrivAt_baseSet 📖	mathematical	—	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTrivAt	—	FiberBundleCore.mem_localTrivAt_baseSet
mem_localTriv_source 📖	mathematical	—	TotalSpace Set Bundle.TotalSpace Fiber Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTriv baseSet	—	—
mem_localTriv_target 📖	mathematical	—	Set Set.instMembership PartialEquiv.target Bundle.TotalSpace Fiber OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTriv Trivialization.baseSet	—	FiberBundleCore.mem_localTriv_target
mem_source_at 📖	mathematical	—	Bundle.TotalSpace Fiber Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toTopologicalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTrivAt	—	localTrivAt.eq_1 mem_localTriv_source mem_baseSet_at
mem_trivChange_source 📖	mathematical	—	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup trivChange Set.instInter baseSet	—	FiberBundleCore.mem_trivChange_source
toFiberBundleCore_baseSet 📖	mathematical	—	FiberBundleCore.baseSet UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFiberBundleCore baseSet	—	—
toFiberBundleCore_coordChange 📖	mathematical	—	FiberBundleCore.coordChange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFiberBundleCore DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange	—	—
toFiberBundleCore_indexAt 📖	mathematical	—	FiberBundleCore.indexAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toFiberBundleCore indexAt	—	—
trivializationAt 📖	mathematical	—	FiberBundle.trivializationAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Fiber toTopologicalSpace topologicalSpaceFiber fiberBundle localTrivAt	—	—
trivializationAt_continuousLinearMapAt 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj FiberBundle.trivializationAt topologicalSpaceFiber fiberBundle	Trivialization.continuousLinearMapAt ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber trivialization_linear vectorBundle instMemTrivializationAtlasTrivializationAt coordChange indexAt	—	localTriv_continuousLinearMapAt
trivializationAt_coordChange_eq 📖	mathematical	Set Set.instMembership Set.instInter Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj FiberBundle.trivializationAt topologicalSpaceFiber fiberBundle	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike Trivialization.coordChangeL moduleFiber trivialization_linear vectorBundle instMemTrivializationAtlasTrivializationAt ContinuousLinearMap ContinuousLinearMap.funLike coordChange indexAt	—	localTriv_coordChange_eq
trivializationAt_symmL 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj FiberBundle.trivializationAt topologicalSpaceFiber fiberBundle	Trivialization.symmL ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber trivialization_linear vectorBundle instMemTrivializationAtlasTrivializationAt coordChange indexAt	—	localTriv_symmL
vectorBundle 📖	mathematical	—	VectorBundle Fiber ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber toTopologicalSpace fiberBundle	—	localTriv.isLinear SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids ContinuousOn.congr continuousOn_coordChange ContinuousLinearMap.ext localTriv_coordChange_eq

VectorBundleCore.localTriv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLinear 📖	mathematical	—	Trivialization.IsLinear VectorBundleCore.Fiber DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup VectorBundleCore.toTopologicalSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule VectorBundleCore.topologicalSpaceFiber VectorBundleCore.moduleFiber VectorBundleCore.localTriv	—	map_add SemilinearMapClass.toAddHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass

VectorPrebundle

Definitions

Name	Category	Theorems
coordChange 📖	CompOp	3 math math: mk_coordChange, continuousOn_coordChange, coordChange_apply
pretrivializationAt 📖	CompOp	5 math math: pretrivialization_mem_atlas, totalSpaceMk_isInducing, mem_trivialization_at_source, mem_base_pretrivializationAt, totalSpaceMk_preimage_source
pretrivializationAtlas 📖	CompOp	1 math math: pretrivialization_mem_atlas
toFiberBundle 📖	CompOp	2 math math: toVectorBundle, contMDiffVectorBundle
toFiberPrebundle 📖	CompOp	—
totalSpaceTopology 📖	CompOp	4 math math: linear_trivializationOfMemPretrivializationAtlas, toVectorBundle, contMDiffVectorBundle, continuous_totalSpaceMk
trivializationOfMemPretrivializationAtlas 📖	CompOp	1 math math: linear_trivializationOfMemPretrivializationAtlas

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_coordChange 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup coordChange Set.instInter Pretrivialization.baseSet	—	SeminormedAddCommGroup.toIsTopologicalAddGroup exists_coordChange
continuous_totalSpaceMk 📖	mathematical	—	Continuous Bundle.TotalSpace totalSpaceTopology	—	FiberPrebundle.continuous_totalSpaceMk
coordChange_apply 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas Set.instInter Pretrivialization.baseSet	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange Pretrivialization.toFun' Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup exists_coordChange
exists_coordChange 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Set.instInter Pretrivialization.baseSet DFunLike.coe ContinuousLinearMap.funLike Pretrivialization.toFun' Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
linear_trivializationOfMemPretrivializationAtlas 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	Trivialization.IsLinear DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField totalSpaceTopology ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule trivializationOfMemPretrivializationAtlas	—	Pretrivialization.IsLinear.linear pretrivialization_linear'
mem_base_pretrivializationAt 📖	mathematical	—	Set Set.instMembership Pretrivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj pretrivializationAt	—	—
mem_trivialization_at_source 📖	mathematical	—	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source Pretrivialization.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj pretrivializationAt	—	FiberPrebundle.mem_pretrivializationAt_source
mk_coordChange 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas Set.instInter Pretrivialization.baseSet	DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike coordChange Pretrivialization.toFun' Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Pretrivialization.mk_symm Pretrivialization.coe_fst' Pretrivialization.proj_symm_apply' coordChange_apply
pretrivialization_linear' 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	Pretrivialization.IsLinear DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	—
pretrivialization_mem_atlas 📖	mathematical	—	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas pretrivializationAt	—	—
toVectorBundle 📖	mathematical	—	VectorBundle totalSpaceTopology toFiberBundle	—	linear_trivializationOfMemPretrivializationAtlas SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids ContinuousOn.congr continuousOn_coordChange ContinuousLinearMap.ext coordChange_apply ContinuousLinearEquiv.coe_coe Trivialization.coordChangeL_apply
totalSpaceMk_isInducing 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace Pretrivialization.toFun' Bundle.TotalSpace.proj pretrivializationAt	—	—
totalSpaceMk_preimage_source 📖	mathematical	—	Set.preimage Bundle.TotalSpace PartialEquiv.source Pretrivialization.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj pretrivializationAt Set.univ	—	FiberPrebundle.totalSpaceMk_preimage_source

(root)

Definitions

Name	Category	Theorems
VectorBundle 📖	CompData	7 math math: Bundle.ContinuousLinearMap.vectorBundle, Bundle.Trivial.vectorBundle, VectorPrebundle.toVectorBundle, TangentSpace.vectorBundle, VectorBundleCore.vectorBundle, VectorBundle.pullback, VectorBundle.prod
VectorBundleCore 📖	CompData	—
VectorPrebundle 📖	CompData	—
instInhabitedVectorBundleCore 📖	CompOp	—
trivialVectorBundleCore 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_coordChange 📖	mathematical	—	ContinuousOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear Set Set.instInter Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	VectorBundle.continuousOn_coordChange'
trivialization_linear 📖	mathematical	—	Trivialization.IsLinear DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	VectorBundle.trivialization_linear'

---

← Back to Index