Basic

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

Statistics

Metric	Count
Definitions IsLinear, linearEquivAt, linearMapAt, symmₗ, IsLinear, continuousLinearEquivAt, continuousLinearMapAt, coordChangeL, linearEquivAt, linearMapAt, symmL, symmₗ, zeroSection, inCoordinates, VectorBundle, continuousLinearEquivAt, 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	41
Theorems 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_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, linearMapAt_symmₗ, mk_coordChangeL, symmL_apply, symmL_continuousLinearMapAt, symm_apply_eq_mk_continuousLinearEquivAt_symm, symm_continuousLinearEquivAt_eq, symm_continuousLinearEquivAt_eq', symm_coordChangeL, symm_linearMapAt, symmₗ_linearMapAt, isLinear, zeroSection, zeroSection_proj, zeroSection_snd, inCoordinates_eq, continuousLinearEquivAt_apply, continuousLinearEquivAt_symm_apply, 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	107
Total	148

Bundle

Definitions

Name	Category	Theorems
zeroSection 📖	CompOp	12 math math: TangentBundle.tangentMap_tangentBundle_pure, contMDiffOn_zeroSection, contMDiffWithinAt_zeroSection, zeroSection_proj, zeroSection_snd, contMDiffAt_zeroSection, Trivialization.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	—	—

Bundle.Pretrivialization

Definitions

Name	Category	Theorems
IsLinear 📖	CompData	3 math math: continuousLinearMap.isLinear, Bundle.Trivialization.toPretrivialization.isLinear, VectorPrebundle.pretrivialization_linear'
linearEquivAt 📖	CompOp	3 math math: linearMapAt_def_of_mem, linearEquivAt_symm_apply, linearEquivAt_apply
linearMapAt 📖	CompOp	8 math math: linearMapAt_eq_zero, linearMapAt_def_of_mem, linearMapAt_symmₗ, coe_linearMapAt_of_mem, symmₗ_linearMapAt, coe_linearMapAt, linearMapAt_apply, linearMapAt_def_of_notMem
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' Bundle.TotalSpace Bundle.TotalSpace.proj	—	coe_linearMapAt
linear 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	IsLinearMap toFun' Bundle.TotalSpace Bundle.TotalSpace.proj	—	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' Bundle.TotalSpace Bundle.TotalSpace.proj	—	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

Bundle.Pretrivialization.IsLinear

Theorems

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

Bundle.Trivialization

Definitions

Name	Category	Theorems
IsLinear 📖	CompData	7 math math: trivialization_linear, VectorBundle.trivialization_linear', VectorPrebundle.linear_trivializationOfMemPretrivializationAtlas, Bundle.Trivial.trivialization.isLinear, prod.isLinear, pullback_linear, VectorBundleCore.localTriv.isLinear
continuousLinearEquivAt 📖	CompOp	14 math math: symm_continuousLinearEquivAt_eq, Bundle.Trivial.continuousLinearEquivAt_trivialization, symm_continuousLinearEquivAt_eq', symm_apply_eq_mk_continuousLinearEquivAt_symm, coe_continuousLinearEquivAt_eq, continuousLinearEquivAt_apply', comp_continuousLinearEquivAt_eq_coord_change, continuousLinearEquivAt_prod, prod_apply', continuousLinearEquivAt_apply, apply_eq_prod_continuousLinearEquivAt, continuousLinearEquivAt_symm_apply, ContinuousLinearMap.inCoordinates_eq, coe_continuousLinearEquivAt_eq'
continuousLinearMapAt 📖	CompOp	18 math math: TangentBundle.continuousLinearMapAt_model_space, VectorBundleCore.localTriv_continuousLinearMapAt, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, Bundle.Pretrivialization.continuousLinearMap_apply, Bundle.Trivial.continuousLinearMapAt_trivialization, coe_continuousLinearEquivAt_eq, VectorBundleCore.trivializationAt_continuousLinearMapAt, continuousLinearMapAt_symmL, symmL_continuousLinearMapAt, Bundle.Pretrivialization.continuousLinearMap_symm_apply, eventually_norm_symmL_trivializationAt_self_comp_lt, TangentBundle.continuousLinearMapAt_trivializationAt, eventually_norm_symmL_trivializationAt_comp_self_lt, continuousLinearMapAt_apply, continuousLinearMap_apply, Bundle.Pretrivialization.continuousLinearMap_symm_apply', eventually_norm_trivializationAt_lt, coe_continuousLinearEquivAt_eq'
coordChangeL 📖	CompOp	30 math math: ContMDiffAt.coordChangeL, MDifferentiable.coordChangeL, coordChangeL_apply, mdifferentiableOn_symm_coordChangeL, VectorBundleCore.trivializationAt_coordChange_eq, comp_continuousLinearEquivAt_eq_coord_change, ContMDiffOn.coordChangeL, MDifferentiableOn.coordChangeL, contMDiffAt_coordChangeL, apply_symm_apply_eq_coordChangeL, MDifferentiableWithinAt.coordChangeL, symm_coordChangeL, coe_coordChangeL, VectorBundle.continuousOn_coordChange', contMDiffOn_symm_coordChangeL, VectorBundleCore.localTriv_coordChange_eq, coordChangeL_prod, mdifferentiableOn_coordChangeL, coordChangeL_symm_apply, ContMDiffVectorBundle.contMDiffOn_coordChangeL, MDifferentiableAt.coordChangeL, ContMDiffWithinAt.coordChangeL, Bundle.Trivial.trivialization.coordChangeL, mk_coordChangeL, mdifferentiableAt_coordChangeL, coordChangeL_apply', contMDiffOn_coordChangeL, coe_coordChangeL', continuousOn_coordChange, ContMDiff.coordChangeL
linearEquivAt 📖	CompOp	6 math math: linearEquivAt_symm_apply, linearMapAt_def_of_mem, coe_coordChangeL, linearEquivAt_apply, coordChangeL_symm_apply, coe_coordChangeL'
linearMapAt 📖	CompOp	12 math math: linearMapAt_def_of_mem, Bundle.Trivial.linearMapAt_trivialization, inCoordinates_apply_eq₂, coe_linearMapAt_of_mem, linearMapAt_symm, linearMapAt_def_of_notMem, linearMapAt_apply, continuousLinearMapAt_apply, symm_linearMapAt, symmₗ_linearMapAt, linearMapAt_symmₗ, coe_linearMapAt
symmL 📖	CompOp	18 math math: symm_continuousLinearEquivAt_eq, symm_continuousLinearEquivAt_eq', Bundle.Trivial.symmL_trivialization, VectorBundleCore.trivializationAt_symmL, TangentBundle.symmL_trivializationAt, VectorBundleCore.localTriv_symmL, TangentBundle.symmL_trivializationAt_eq_core, Bundle.Pretrivialization.continuousLinearMap_apply, continuousLinearMapAt_symmL, symmL_continuousLinearMapAt, Bundle.Pretrivialization.continuousLinearMap_symm_apply, eventually_norm_symmL_trivializationAt_self_comp_lt, eventually_norm_symmL_trivializationAt_comp_self_lt, symmL_apply, eventually_norm_symmL_trivializationAt_lt, TangentBundle.symmL_model_space, continuousLinearMap_apply, Bundle.Pretrivialization.continuousLinearMap_symm_apply'
symmₗ 📖	CompOp	4 math math: coe_symmₗ, symmₗ_linearMapAt, linearMapAt_symmₗ, 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' 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	—	RingHomInvPair.ids coe_fst source_eq
apply_symm_apply_eq_coordChangeL 📖	mathematical	Set Set.instMembership Set.instInter baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	toFun' Bundle.TotalSpace Bundle.TotalSpace.proj 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt ContinuousLinearMap ContinuousLinearMap.funLike continuousLinearMapAt	—	coe_linearMapAt_of_mem
coe_continuousLinearEquivAt_eq' 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule continuousLinearEquivAt continuousLinearMapAt	—	DFunLike.coe_injective RingHomInvPair.ids 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 Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	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 Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	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	—	Bundle.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' Bundle.TotalSpace Bundle.TotalSpace.proj	—	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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearEquiv.symm continuousLinearEquivAt Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt toFun' Bundle.TotalSpace Bundle.TotalSpace.proj	—	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 Bundle.TotalSpace.proj UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd toOpenPartialHomeomorph 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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' Bundle.TotalSpace Bundle.TotalSpace.proj 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' Bundle.TotalSpace Bundle.TotalSpace.proj 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 Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	RingHomInvPair.ids
linear 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	IsLinearMap toFun' Bundle.TotalSpace Bundle.TotalSpace.proj	—	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' Bundle.TotalSpace Bundle.TotalSpace.proj	—	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 AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Bundle.Pretrivialization.linearMapAt_symmₗ 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ₗ	—	Bundle.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' Bundle.TotalSpace Bundle.TotalSpace.proj 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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' Bundle.TotalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup OpenPartialHomeomorph.symm 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 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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquivAt ContinuousLinearMap ContinuousLinearMap.funLike symmL	—	RingHomInvPair.ids
symm_continuousLinearEquivAt_eq' 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContinuousLinearEquiv.toContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearEquiv.symm continuousLinearEquivAt 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	symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike linearMapAt	—	Bundle.Pretrivialization.symmₗ_linearMapAt toPretrivialization.isLinear
symmₗ_linearMapAt 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike symmₗ linearMapAt	—	Bundle.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.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj 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

Bundle.Trivialization.IsLinear

Theorems

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

Bundle.Trivialization.toPretrivialization

Theorems

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

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 Bundle.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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule RingHomCompTriple.right_ids ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Bundle.Trivialization.continuousLinearEquivAt FiberBundle.trivializationAt trivialization_linear instMemTrivializationAtlasTrivializationAt RingHomCompTriple.ids ContinuousLinearEquiv.symm	—	ext RingHomCompTriple.right_ids RingHomInvPair.ids trivialization_linear instMemTrivializationAtlasTrivializationAt RingHomCompTriple.ids Bundle.Trivialization.coe_continuousLinearEquivAt_eq

VectorBundle

Definitions

Name	Category	Theorems
continuousLinearEquivAt 📖	CompOp	2 math math: continuousLinearEquivAt_apply, continuousLinearEquivAt_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousLinearEquivAt_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike continuousLinearEquivAt Bundle.Trivialization.toFun' Bundle.TotalSpace Bundle.TotalSpace.proj FiberBundle.trivializationAt	—	RingHomInvPair.ids
continuousLinearEquivAt_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm continuousLinearEquivAt Bundle.Trivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid FiberBundle.trivializationAt	—	RingHomInvPair.ids
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 NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Bundle.Trivialization.coordChangeL trivialization_linear' Set Set.instInter Bundle.Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	—
trivialization_linear' 📖	mathematical	—	Bundle.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	9 math math: trivializationAt_symmL, localTriv_continuousLinearMapAt, localTriv_symmL, trivializationAt_coordChange_eq, trivializationAt_continuousLinearMapAt, instContMDiffVectorBundle, inCoordinates_eq, trivializationAt, vectorBundle
indexAt 📖	CompOp	13 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, inCoordinates_eq, tangentBundleCore_indexAt
localTriv 📖	CompOp	12 math math: mem_localTriv_target, localTriv_continuousLinearMapAt, localTriv_symmL, localTriv_symm_fst, localTriv_symm_apply, baseSet_at, localTriv_coordChange_eq, 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	24 math math: trivializationAt_symmL, mem_localTriv_target, localTriv_continuousLinearMapAt, localTriv_symmL, continuous_proj, localTriv_symm_fst, localTrivAt_apply, trivializationAt_coordChange_eq, localTriv_symm_apply, trivializationAt_continuousLinearMapAt, isOpenMap_proj, baseSet_at, mem_source_at, instContMDiffVectorBundle, localTriv_coordChange_eq, localTriv_apply, localTrivAt_apply_mk, tangentBundleCore_localTriv_baseSet, inCoordinates_eq, trivializationAt, mem_localTriv_source, localTriv.isLinear, mem_localTrivAt_baseSet, vectorBundle
topologicalSpaceFiber 📖	CompOp	11 math math: trivializationAt_symmL, localTriv_continuousLinearMapAt, localTriv_symmL, trivializationAt_coordChange_eq, trivializationAt_continuousLinearMapAt, 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 Bundle.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 NormedAddCommGroup.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 indexAt 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	—	Bundle.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	—	Bundle.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	—	Bundle.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 Bundle.Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	Bundle.Trivialization.continuousLinearMapAt Fiber ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber toTopologicalSpace fiberBundle localTriv localTriv.isLinear coordChange indexAt	—	ContinuousLinearMap.ext localTriv.isLinear Bundle.Trivialization.continuousLinearMapAt_apply Bundle.Trivialization.coe_linearMapAt_of_mem
localTriv_coordChange_eq 📖	mathematical	Set Set.instMembership Bundle.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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike Bundle.Trivialization.coordChangeL Fiber toTopologicalSpace topologicalSpaceFiber moduleFiber localTriv localTriv.isLinear ContinuousLinearMap ContinuousLinearMap.funLike coordChange	—	RingHomInvPair.ids localTriv.isLinear Bundle.Trivialization.coordChangeL_apply' localTriv_symm_fst localTriv_apply coordChange_comp mem_baseSet_at
localTriv_symmL 📖	mathematical	Set Set.instMembership Bundle.Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	Bundle.Trivialization.symmL Fiber ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber toTopologicalSpace fiberBundle localTriv localTriv.isLinear coordChange indexAt	—	ContinuousLinearMap.ext localTriv.isLinear Bundle.Trivialization.symmL_apply Bundle.Trivialization.symm_coe_proj Bundle.Trivialization.symm_apply
localTriv_symm_apply 📖	mathematical	Set Set.instMembership Bundle.Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj localTriv	Bundle.Trivialization.symm Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid addCommGroupFiber 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.Trivialization.symm_apply
localTriv_symm_fst 📖	mathematical	—	OpenPartialHomeomorph.toFun' Bundle.TotalSpace Fiber instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace OpenPartialHomeomorph.symm Bundle.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 Bundle.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 Bundle.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 Bundle.Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj localTriv Bundle.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 Bundle.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 Bundle.Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj FiberBundle.trivializationAt topologicalSpaceFiber fiberBundle	Bundle.Trivialization.continuousLinearMapAt Fiber ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber toTopologicalSpace fiberBundle FiberBundle.trivializationAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup trivialization_linear vectorBundle instMemTrivializationAtlasTrivializationAt coordChange indexAt	—	localTriv_continuousLinearMapAt
trivializationAt_coordChange_eq 📖	mathematical	Set Set.instMembership Set.instInter Bundle.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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike Bundle.Trivialization.coordChangeL Fiber toTopologicalSpace topologicalSpaceFiber moduleFiber FiberBundle.trivializationAt fiberBundle trivialization_linear vectorBundle instMemTrivializationAtlasTrivializationAt ContinuousLinearMap ContinuousLinearMap.funLike coordChange indexAt	—	localTriv_coordChange_eq
trivializationAt_symmL 📖	mathematical	Set Set.instMembership Bundle.Trivialization.baseSet Bundle.TotalSpace Fiber UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toTopologicalSpace Bundle.TotalSpace.proj FiberBundle.trivializationAt topologicalSpaceFiber fiberBundle	Bundle.Trivialization.symmL Fiber ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber toTopologicalSpace fiberBundle FiberBundle.trivializationAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup 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	—	Bundle.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	Bundle.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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup coordChange Set Set.instInter Bundle.Pretrivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	SeminormedAddCommGroup.toIsTopologicalAddGroup exists_coordChange
continuous_totalSpaceMk 📖	mathematical	—	Continuous Bundle.TotalSpace totalSpaceTopology	—	FiberPrebundle.continuous_totalSpaceMk
coordChange_apply 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas Set.instInter Bundle.Pretrivialization.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 Bundle.Pretrivialization.toFun' Bundle.TotalSpace Bundle.TotalSpace.proj Bundle.Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	SeminormedAddCommGroup.toIsTopologicalAddGroup exists_coordChange
exists_coordChange 📖	mathematical	Bundle.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 UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Set Set.instInter Bundle.Pretrivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj DFunLike.coe ContinuousLinearMap.funLike Bundle.Pretrivialization.toFun' Bundle.Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
linear_trivializationOfMemPretrivializationAtlas 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	Bundle.Trivialization.IsLinear DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup totalSpaceTopology ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule trivializationOfMemPretrivializationAtlas	—	Bundle.Pretrivialization.IsLinear.linear pretrivialization_linear'
mem_base_pretrivializationAt 📖	mathematical	—	Set Set.instMembership Bundle.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 Bundle.Pretrivialization.toPartialEquiv UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj pretrivializationAt	—	FiberPrebundle.mem_pretrivializationAt_source
mk_coordChange 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas Set.instInter Bundle.Pretrivialization.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 Bundle.Pretrivialization.toFun' Bundle.TotalSpace Bundle.TotalSpace.proj Bundle.Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Bundle.Pretrivialization.mk_symm Bundle.Pretrivialization.coe_fst' Bundle.Pretrivialization.proj_symm_apply' coordChange_apply
pretrivialization_linear' 📖	mathematical	Bundle.Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	Bundle.Pretrivialization.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	—	—
pretrivialization_mem_atlas 📖	mathematical	—	Bundle.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 Bundle.Trivialization.coordChangeL_apply
totalSpaceMk_isInducing 📖	mathematical	—	Topology.IsInducing instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace Bundle.Pretrivialization.toFun' Bundle.TotalSpace.proj pretrivializationAt	—	—
totalSpaceMk_preimage_source 📖	mathematical	—	Set.preimage Bundle.TotalSpace PartialEquiv.source Bundle.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 NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Bundle.Trivialization.coordChangeL trivialization_linear Set Set.instInter Bundle.Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	VectorBundle.continuousOn_coordChange'
trivialization_linear 📖	mathematical	—	Bundle.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