Structures · Topology
MemTrivializationAtlas
Given a type E equipped with a fiber bundle structure, this is a Prop typeclass
for trivializations of E, expressing that a trivialization is in the designated atlas for the
bundle. This is needed because lemmas about the linearity of trivializations or the continuity (as
functions to F →L[R] F, where F is the model fiber) of the transition functions are only
expected to hold for trivializations in the designated atlas.
- Defined in
- Mathlib.Topology.FiberBundle.Basic
- Shape
- One type argument · adds out
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 by112
- Bundle.Trivialization.localFrameCoeff
- Bundle.Trivialization.localFrame
- Bundle.Trivialization.isLocalFrameOn_localFrame_baseSet
- Bundle.Trivialization.basisAt
- Bundle.Trivialization.continuousLinearMap
- contMDiffOn_coordChangeL
- mdifferentiableAt_localFrameCoeff
- contMDiffAt_localFrameCoeff
- ContMDiffVectorBundle.contMDiffOn_coordChangeL
- MDifferentiableWithinAt.coordChangeL
- contMDiffAt_coordChangeL
- Bundle.Trivialization.localFrameCoeff_eq_coeff
- MDifferentiableWithinAt.coordChange
- ContMDiffWithinAt.coordChange
- contMDiffOn_localFrameCoeff
- Bundle.Trivialization.contMDiffWithinAt_iff
- ContMDiffWithinAt.coordChangeL
- Bundle.Trivialization.continuousAlternatingMap
- Bundle.Trivialization.mdifferentiableWithinAt_snd_comp_iff₂
- continuousOn_coordChange
- mdifferentiableOn_localFrameCoeff
- Bundle.Trivialization.contMDiffOn_iff
- Bundle.Trivialization.eq_sum_localFrameCoeff_smul
- Bundle.Trivialization.contMDiffWithinAt_section
- Bundle.Trivialization.mdifferentiableAt_section_iff
- Bundle.Trivialization.contMDiffAt_section_iff
- Bundle.Trivialization.localFrame_apply_of_mem_baseSet
- contMDiffAt_iff_localFrameCoeff
- contMDiffOn_iff_localFrameCoeff
- Bundle.Trivialization.localFrameCoeff_apply_of_mem_baseSet
- Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff
- Bundle.Trivialization.contMDiffOn_symm
- contMDiffAt_localFrame_of_mem
- Bundle.Trivialization.localFrameCoeff_congr
- Bundle.Trivialization.mdifferentiableOn_section_iff
- MDifferentiableAt.coordChange
- contMDiffOn_symm_coordChangeL
- mdifferentiableAt_coordChangeL
- MemTrivializationAtlas.out
- MDifferentiableAt.coordChangeL
- mdifferentiableAt_iff_localFrameCoeff
- Bundle.Trivialization.contMDiffOn_section_iff
- MDifferentiableWithinAt.change_section_trivialization
- ContMDiffOn.coordChange
- Bundle.Trivialization.mdifferentiableWithinAt_section_iff
- ContMDiffWithinAt.change_section_trivialization
- VectorBundle.trivialization_linear'
- Bundle.Trivialization.contMDiffOn_localFrame_baseSet
- contMDiffOn_baseSet_iff_localFrameCoeff
- Bundle.Trivialization.contMDiffOn
Ancestors0
No ancestors.