Constructions

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

Statistics

Metric	Count
Definitions instAddCommMonoidPullback, instModulePullback	2
Theorems continuousLinearEquivAt_trivialization, continuousLinearMapAt_trivialization, linearMapAt_trivialization, symmL_trivialization, symmₗ_trivialization, coordChangeL, isLinear, vectorBundle, continuousLinearEquivAt_prod, coordChangeL_prod, isLinear, prod_apply', pullback_linear, prod, pullback	15
Total	17

Bundle.Trivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousLinearEquivAt_trivialization 📖	mathematical	—	Trivialization.continuousLinearEquivAt Bundle.Trivial ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NontriviallyNormedField.toNormedField topologicalSpace fiberBundle trivialization trivialization.isLinear Set.mem_univ ContinuousLinearEquiv.refl DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	ContinuousLinearEquiv.ext RingHomInvPair.ids trivialization.isLinear Set.mem_univ
continuousLinearMapAt_trivialization 📖	mathematical	—	Trivialization.continuousLinearMapAt Bundle.Trivial ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NontriviallyNormedField.toNormedField topologicalSpace fiberBundle trivialization trivialization.isLinear ContinuousLinearMap.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	ContinuousLinearMap.ext trivialization.isLinear linearMapAt_trivialization
linearMapAt_trivialization 📖	mathematical	—	Trivialization.linearMapAt Bundle.Trivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup topologicalSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule trivialization trivialization.isLinear LinearMap.id	—	LinearMap.ext trivialization.isLinear Trivialization.coe_linearMapAt_of_mem
symmL_trivialization 📖	mathematical	—	Trivialization.symmL Bundle.Trivial ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NontriviallyNormedField.toNormedField topologicalSpace fiberBundle trivialization trivialization.isLinear ContinuousLinearMap.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	ContinuousLinearMap.ext trivialization.isLinear trivialization_symm_apply
symmₗ_trivialization 📖	mathematical	—	Trivialization.symmₗ Bundle.Trivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup topologicalSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule trivialization trivialization.isLinear LinearMap.id	—	LinearMap.ext trivialization.isLinear trivialization_symm_apply
vectorBundle 📖	mathematical	—	VectorBundle Bundle.Trivial ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NontriviallyNormedField.toNormedField topologicalSpace fiberBundle	—	eq_trivialization trivialization.isLinear SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization.coordChangeL Continuous.continuousOn continuous_const

Bundle.Trivial.trivialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coordChangeL 📖	mathematical	—	Trivialization.coordChangeL Bundle.Trivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.Trivial.topologicalSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Bundle.Trivial.trivialization isLinear ContinuousLinearEquiv.refl	—	ContinuousLinearEquiv.ext RingHomInvPair.ids isLinear Trivialization.coordChangeL_apply' Set.mem_univ
isLinear 📖	mathematical	—	Trivialization.IsLinear Bundle.Trivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.Trivial.topologicalSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Bundle.Trivial.trivialization	—	—

Trivialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousLinearEquivAt_prod 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup FiberBundle.Prod.topologicalSpace Bundle.TotalSpace.proj prod AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	continuousLinearEquivAt Prod.instAddCommMonoid Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Prod.normedAddCommGroup Prod.normedSpace FiberBundle.prod PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup prod.isLinear ContinuousLinearEquiv.prodCongr ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	ContinuousLinearEquiv.ext RingHomInvPair.ids prod.isLinear continuousLinearEquivAt_apply Prod.left_inv Prod.right_inv Prod.continuous_to_fun Prod.continuous_inv_fun prod.eq_1 prod_apply'
coordChangeL_prod 📖	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 instTopologicalSpaceProd Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule NormedSpace.toModule coordChangeL FiberBundle.Prod.topologicalSpace prod AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid prod.isLinear ContinuousLinearMap.prodMap	—	RingHomInvPair.ids prod.isLinear ContinuousLinearMap.ext_iff ContinuousLinearMap.coe_prodMap' coordChangeL_apply coordChangeL_apply'
prod_apply' 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	toFun' instTopologicalSpaceProd FiberBundle.Prod.topologicalSpace prod AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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	—	—
pullback_linear 📖	mathematical	—	IsLinear Bundle.Pullback DFunLike.coe DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Pullback.TotalSpace.topologicalSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule instAddCommMonoidPullback instModulePullback pullback AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	linear

Trivialization.prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLinear 📖	mathematical	—	Trivialization.IsLinear DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup FiberBundle.Prod.topologicalSpace Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Prod.instModule NormedSpace.toModule Trivialization.prod AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LinearMap.isLinear Trivialization.linear

VectorBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	—	VectorBundle Prod.instAddCommMonoid Prod.instModule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Prod.normedAddCommGroup Prod.normedSpace NormedAddCommGroup.toSeminormedAddCommGroup FiberBundle.Prod.topologicalSpace instTopologicalSpaceProd FiberBundle.prod UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Trivialization.prod.isLinear trivialization_linear SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids ContinuousOn.congr Prod.instIsTopologicalAddGroup ContinuousOn.prod_mapL ContinuousOn.mono continuousOn_coordChange ContinuousLinearMap.ext_iff Trivialization.coordChangeL_apply Trivialization.coordChangeL_apply'
pullback 📖	mathematical	—	VectorBundle Bundle.Pullback DFunLike.coe instAddCommMonoidPullback instModulePullback DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Pullback.TotalSpace.topologicalSpace instTopologicalSpacePullback FiberBundle.pullback UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Trivialization.pullback_linear trivialization_linear SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids ContinuousOn.congr ContinuousOn.comp continuousOn_coordChange Continuous.continuousOn ContinuousMapClass.map_continuous ContinuousLinearMap.ext Trivialization.coordChangeL_apply Trivialization.coordChangeL_apply'

(root)

Definitions

Name	Category	Theorems
instAddCommMonoidPullback 📖	CompOp	3 math math: Trivialization.pullback_linear, ContMDiffVectorBundle.pullback, VectorBundle.pullback
instModulePullback 📖	CompOp	3 math math: Trivialization.pullback_linear, ContMDiffVectorBundle.pullback, VectorBundle.pullback

---

← Back to Index