Structures · Topology
VectorBundle
The space Bundle.TotalSpace F E (for E : B → Type* such that each E x is a topological
vector space) has a topological vector space structure with fiber F (denoted with
VectorBundle R F E) if around every point there is a fiber bundle trivialization which is linear
in the fibers.
- Defined in
- Mathlib.Topology.VectorBundle.Basic
- Shape
- 3 explicit arguments · adds trivialization_linear', continuousOn_coordChange'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by365
- Bundle.Trivialization.localFrameCoeff
- ContinuousLinearMap.inCoordinates
- Bundle.Trivialization.localFrame
- Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet
- Bundle.contMDiff_zeroSection
- ContinuousLinearMap.inCoordinates_eq
- IsLocalFrameOn.fintypeOfFiniteDimensional
- Bundle.Trivialization.basisAt
- CovariantDerivative.derivMetricTensor
- Bundle.Trivialization.continuousLinearMap
- ContMDiffOn.smul_section
- Bundle.mdifferentiable_zeroSection
- MDifferentiableAt.sum_section
- ContMDiffWithinAt.clm_apply_of_inCoordinates
- mdifferentiableWithinAt_add_section
- ContMDiffWithinAt.add_section
- contMDiffOn_coordChangeL
- mdifferentiableAt_localFrameCoeff
- ContinuousAlternatingMap.inCoordinates
- Bundle.ContMDiffRiemannianMetric.inner
- Bundle.ContinuousRiemannianMetric.inner
- MDifferentiableAt.smul_section
- VectorBundle.continuousLinearEquivAt
- TensorialAt.mkHom
- ContMDiffWithinAt.sum_section
- ContMDiffWithinAt.neg_section
- contMDiffAt_localFrameCoeff
- MDifferentiableWithinAt.smul_section
- ContMDiffWithinAt.clm_bundle_apply₂
- MDifferentiableWithinAt.sum_section_of_locallyFinite
- MDifferentiableWithinAt.coordChangeL
- contMDiffAt_coordChangeL
- ContMDiffWithinAt.smul_section
- Bundle.Trivialization.localFrameCoeff_eq_coeff
- MDifferentiableWithinAt.clm_bundle_apply₂
- MDifferentiableWithinAt.coordChange
- ContMDiffWithinAt.coordChange
- TensorialAt.mkHom₂_apply
- contMDiffOn_localFrameCoeff
- MDifferentiableOn.smul_section
- ContMDiffWithinAt.sum_section_of_locallyFinite
- mdifferentiableWithinAt_neg_section
- MDifferentiableWithinAt.clm_apply_of_inCoordinates
- ContMDiffWithinAt.clm_bundle_apply
- MDifferentiableWithinAt.clm_bundle_apply
- Bundle.Trivialization.contMDiffWithinAt_iff
- ContMDiffWithinAt.coordChangeL
- ContMDiffAt.smul_section
- ContinuousWithinAt.clm_bundle_apply
- TensorialAt.mkHom₂
Ancestors0
No ancestors.