Structures · Topology
FiberBundle
A (topological) fiber bundle with fiber F over a base B is a space projecting on B
for which the fibers are all homeomorphic to F, such that the local situation around each point
is a direct product.
- Defined in
- Mathlib.Topology.FiberBundle.Basic
- Shape
- 2 explicit arguments · adds totalSpaceMk_isInducing', trivializationAtlas', trivializationAt', mem_baseSet_trivializationAt', trivialization_mem_atlas'
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 by540
- FiberBundle.trivializationAt
- Bundle.Trivialization.localFrameCoeff
- Bundle.Trivialization.continuousLinearMapAt
- Bundle.Trivialization.symmL
- Bundle.Trivialization.continuousLinearEquivAt
- ContinuousLinearMap.inCoordinates
- FiberBundle.mem_baseSet_trivializationAt'
- FiberBundle.mem_baseSet_trivializationAt
- CovariantDerivative.toFun
- FiberBundle.extend
- IsLocalFrameOn.coeff
- Bundle.Trivialization.symmL_apply
- Bundle.Trivialization.continuousLinearMapAt_apply
- Bundle.Trivialization.localFrame
- Bundle.Trivialization.continuousLinearEquivAt_apply
- Bundle.Trivialization.continuousLinearEquivAt_symm_apply
- IsLocalFrameOn.toBasisAt
- Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet
- IsLocalFrameOn.contMDiffOn
- Bundle.contMDiff_zeroSection
- IsCovariantDerivativeOn.leibniz
- FiberBundle.chartedSpace_chartAt
- IsCovariantDerivativeOn.add
- FiberBundle.extend_apply_self
- ContinuousLinearMap.inCoordinates_eq
- IsLocalFrameOn.fintypeOfFiniteDimensional
- FiberBundle.continuous_proj
- Bundle.Trivialization.basisAt
- CovariantDerivative.derivMetricTensor
- Bundle.Pretrivialization.continuousAlternatingMap
- Bundle.Trivialization.continuousLinearMap
- Bundle.Pretrivialization.continuousLinearMap
- IsLocalFrameOn.coeff_sum_eq
- IsLocalFrameOn.generating
- FiberBundle.continuousWithinAt_totalSpace
- FiberBundle.mem_trivializationAt_proj_source
- Bundle.contMDiffWithinAt_totalSpace
- mdifferentiableWithinAt_totalSpace
- ContMDiffOn.smul_section
- Bundle.Trivialization.coe_continuousLinearEquivAt_eq
- IsLocalFrameOn.linearIndependent
- Bundle.mdifferentiable_zeroSection
- FiberBundle.trivializationAt'
- Bundle.contMDiffWithinAt_section
- FiberBundle.trivializationAtlas
- mdifferentiableWithinAt_section
- MDifferentiableAt.sum_section
- FiberBundle.trivializationAtlas'
- ContMDiffWithinAt.clm_apply_of_inCoordinates
- mdifferentiableWithinAt_add_section
Ancestors0
No ancestors.