Basic

📁 Source: Mathlib/Geometry/Manifold/VectorBundle/Basic.lean

Statistics

Metric	Count
Definitions ContMDiffVectorBundle, chartedSpace, chartedSpace', IsContMDiff, IsContMDiff, contMDiffCoordChange	6
Theorems contMDiffVectorBundle, isManifold, contMDiffVectorBundle, contMDiffAt_proj, contMDiffAt_section, contMDiffAt_totalSpace, contMDiffAt_zeroSection, contMDiffOn_proj, contMDiffOn_zeroSection, contMDiffWithinAt_proj, contMDiffWithinAt_section, contMDiffWithinAt_totalSpace, contMDiffWithinAt_zeroSection, contMDiff_proj, contMDiff_zeroSection, coordChange, coordChangeL, coordChange, coordChangeL, hasGroupoid, coordChange, coordChangeL, contMDiffOn_coordChangeL, of_le, change_section_trivialization, coordChange, coordChangeL, chartedSpace'_chartAt, chartedSpace_chartAt, chartedSpace_chartAt_symm_fst, extChartAt, extChartAt_target, writtenInExtChartAt_trivializationAt, writtenInExtChartAt_trivializationAt_symm, contMDiffAt_iff, contMDiffAt_section_iff, contMDiffOn, contMDiffOn_iff, contMDiffOn_section_baseSet_iff, contMDiffOn_section_iff, contMDiffOn_symm, contMDiffOn_symm_trans, contMDiffWithinAt_iff, contMDiffWithinAt_section, contMDiffWithinAt_snd_comp_iff₂, contMDiff_iff, contMDiffOn_coordChange, contMDiffOn_coordChange, instContMDiffVectorBundle, exists_contMDiffCoordChange, contMDiffCoordChange_apply, contMDiffOn_contMDiffCoordChange, contMDiffVectorBundle, mk_contMDiffCoordChange, contMDiffAt_coordChangeL, contMDiffAt_section_of_mem_baseSet, contMDiffOn_coordChangeL, contMDiffOn_section_of_mem_baseSet, contMDiffOn_section_of_mem_baseSet₀, contMDiffOn_symm_coordChangeL, instContMDiffVectorBundleOfNatWithTopENat, instContMDiffVectorBundleOfNatWithTopENat_1, instContMDiffVectorBundleOfSomeENatTopOfLEInfty, instContMDiffVectorBundleOfTopWithTopENat	64
Total	70

Bundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_proj 📖	mathematical	—	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.proj	—	ContMDiff.contMDiffAt contMDiff_proj
contMDiffAt_section 📖	mathematical	—	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.mk' chartedSpaceSelf Trivialization.toFun' TotalSpace.proj FiberBundle.trivializationAt	—	contMDiffAt_id
contMDiffAt_totalSpace 📖	mathematical	—	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.proj chartedSpaceSelf Trivialization.toFun' FiberBundle.trivializationAt	—	contMDiffWithinAt_totalSpace
contMDiffAt_zeroSection 📖	mathematical	—	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace zeroSection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	ContMDiff.contMDiffAt contMDiff_zeroSection
contMDiffOn_proj 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.proj	—	ContMDiff.contMDiffOn contMDiff_proj
contMDiffOn_zeroSection 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace zeroSection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	ContMDiff.contMDiffOn contMDiff_zeroSection
contMDiffWithinAt_proj 📖	mathematical	—	ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.proj	—	ContMDiffAt.contMDiffWithinAt contMDiffAt_proj
contMDiffWithinAt_section 📖	mathematical	—	ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.mk' chartedSpaceSelf Trivialization.toFun' TotalSpace.proj FiberBundle.trivializationAt	—	contMDiffWithinAt_id
contMDiffWithinAt_totalSpace 📖	mathematical	—	ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.proj chartedSpaceSelf Trivialization.toFun' FiberBundle.trivializationAt	—	FiberBundle.continuousWithinAt_totalSpace modelWithCornersSelf_prod FiberBundle.extChartAt contMDiffWithinAt_prod_iff ContinuousWithinAt.comp Continuous.continuousWithinAt FiberBundle.continuous_proj Set.mapsTo_image IsOpen.mem_nhds Trivialization.open_baseSet FiberBundle.mem_baseSet_trivializationAt Filter.EventuallyEq.contMDiffWithinAt_iff Filter.eventually_of_mem Trivialization.coe_fst' Trivialization.coe_fst
contMDiffWithinAt_zeroSection 📖	mathematical	—	ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace zeroSection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	ContMDiffAt.contMDiffWithinAt contMDiff_zeroSection
contMDiff_proj 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace TotalSpace.proj	—	contMDiffAt_id contMDiffAt_totalSpace
contMDiff_zeroSection 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf TotalSpace FiberBundle.chartedSpace zeroSection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	contMDiffAt_section ContMDiffAt.congr_of_eventuallyEq contMDiffAt_const Filter.mp_mem IsOpen.mem_nhds Trivialization.open_baseSet FiberBundle.mem_baseSet_trivializationAt Filter.univ_mem' Trivialization.zeroSection trivialization_linear instMemTrivializationAtlasTrivializationAt

Bundle.Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffVectorBundle 📖	mathematical	—	ContMDiffVectorBundle 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 VectorBundle.prod	—	VectorBundle.prod RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear ContMDiffOn.congr ContMDiffOn.clm_prodMap ContMDiffOn.mono contMDiffOn_coordChangeL Trivialization.coordChangeL_prod

Bundle.TotalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isManifold 📖	mathematical	—	IsManifold Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	—	StructureGroupoid.HasGroupoid.comp IsManifold.toHasGroupoid IsManifold.prod IsManifold.instOfTopWithTopENat instIsManifoldModelSpace instClosedUnderRestrictionContDiffGroupoid ContMDiffFiberwiseLinear.hasGroupoid RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup ContMDiffOn.continuousOn mem_contMDiffFiberwiseLinear_iff isLocalStructomorphOn_contDiffGroupoid_iff ContMDiffOn.congr OpenPartialHomeomorph.EqOnSource.source_eq ContMDiffOn.prodMk contMDiffOn_fst ContMDiffOn.clm_apply ContMDiffOn.comp Set.prod_subset_preimage_fst contMDiffOn_snd OpenPartialHomeomorph.EqOnSource.eqOn OpenPartialHomeomorph.EqOnSource.target_eq OpenPartialHomeomorph.EqOnSource.symm'

Bundle.Trivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffVectorBundle 📖	mathematical	—	ContMDiffVectorBundle Bundle.Trivial ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule NontriviallyNormedField.toNormedField topologicalSpace fiberBundle vectorBundle	—	vectorBundle RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear trivialization.coordChangeL ContMDiff.contMDiffOn contMDiff_const eq_trivialization

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coordChange 📖	mathematical	ContMDiff UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	Trivialization.coordChange	—	ContMDiffAt.coordChange
coordChangeL 📖	mathematical	ContMDiff Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear	—	ContMDiffAt.coordChangeL

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coordChange 📖	mathematical	ContMDiffAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	Trivialization.coordChange	—	ContMDiffWithinAt.coordChange
coordChangeL 📖	mathematical	ContMDiffAt Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear	—	ContMDiffWithinAt.coordChangeL

ContMDiffFiberwiseLinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasGroupoid 📖	mathematical	—	HasGroupoid instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace FiberBundle.chartedSpace' contMDiffFiberwiseLinear	—	RingHomInvPair.ids RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup ContMDiffOn.continuousOn mem_contMDiffFiberwiseLinear_iff trivialization_linear IsOpen.inter Trivialization.open_baseSet contMDiffOn_coordChangeL contMDiffOn_symm_coordChangeL Trivialization.symm_trans_source_eq Trivialization.apply_symm_apply_eq_coordChangeL

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coordChange 📖	mathematical	ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Set.MapsTo Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	Trivialization.coordChange	—	ContMDiffWithinAt.coordChange
coordChangeL 📖	mathematical	ContMDiffOn Set.MapsTo Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear	—	ContMDiffWithinAt.coordChangeL

ContMDiffVectorBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffOn_coordChangeL 📖	mathematical	—	ContMDiffOn 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.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear Set Set.instInter Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	—
of_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	ContMDiffVectorBundle	—	ContMDiffOn.of_le RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear contMDiffOn_coordChangeL

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
change_section_trivialization 📖	—	ContMDiffWithinAt Bundle.TotalSpace Bundle.TotalSpace.proj UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Trivialization.toFun' Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph	—	—	congr_of_eventuallyEq coordChange Trivialization.mem_source Filter.mp_mem continuousWithinAt IsOpen.mem_nhds Trivialization.open_baseSet Filter.univ_mem' Trivialization.coordChange_apply_snd
coordChange 📖	mathematical	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	Trivialization.coordChange	—	congr_of_eventuallyEq RingHomInvPair.ids trivialization_linear clm_apply coordChangeL IsOpen.mem_nhds IsOpen.inter Trivialization.open_baseSet Filter.mp_mem continuousWithinAt Filter.univ_mem' Trivialization.coordChangeL_apply'
coordChangeL 📖	mathematical	ContMDiffWithinAt Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear	—	ContMDiffAt.comp_contMDiffWithinAt RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear contMDiffAt_coordChangeL

FiberBundle

Definitions

Name	Category	Theorems
chartedSpace 📖	CompOp	105 math math: TangentBundle.tangentMap_tangentBundle_pure, Bundle.ContMDiffRiemannianMetric.contMDiff, Bundle.mdifferentiableAt_proj, Trivialization.mdifferentiableAt_section_iff, Bundle.contMDiffOn_zeroSection, mdifferentiableWithinAt_totalSpace, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, tangentMap_chart, contMDiff_addInvariantVectorField, Trivialization.mdifferentiableOn_section_baseSet_iff, TangentBundle.coe_chartAt_fst, Bundle.contMDiffWithinAt_zeroSection, contMDiff_mulInvariantVectorField, IsLocalFrameOn.contMDiffAt_of_coeff, contMDiff_equivTangentBundleProd_symm, mdifferentiableWithinAt_section, Trivialization.contMDiffAt_iff, Trivialization.contMDiff_iff, Trivialization.contMDiffOn_section_iff, tangentBundle_model_space_coe_chartAt, Bundle.contMDiffAt_zeroSection, contMDiffAt_mulInvariantVectorField, mdifferentiableAt_addInvariantVectorField, ContMDiff.contMDiff_tangentMap, mdifferentiableAt_totalSpace, mdifferentiable_mulInvariantVectorField, chartedSpace_chartAt, Trivialization.mdifferentiableAt_totalSpace_iff, mdifferentiableAt_hom_bundle, IsLocalFrameOn.mdifferentiableAt_of_coeff_aux, Bundle.TotalSpace.isManifold, contMDiff_vectorSpace_iff_contDiff, UniqueMDiffWithinAt.bundle_preimage', IsContMDiffRiemannianBundle.exists_contMDiff, IsLocalFrameOn.mdifferentiableOn_of_coeff, Trivialization.contMDiffOn_localFrame_baseSet, Bundle.mdifferentiableWithinAt_proj, IsLocalFrameOn.contMDiffOn, Bundle.contMDiffWithinAt_totalSpace, Bundle.mdifferentiableOn_proj, tangentBundle_model_space_coe_chartAt_symm, TangentBundle.chartAt, IsLocalFrameOn.contMDiffAt, contMDiffAt_hom_bundle, extChartAt, Bundle.contMDiffWithinAt_proj, Bundle.contMDiffAt_totalSpace, Trivialization.contMDiffOn_section_baseSet_iff, UniqueMDiffOn.tangentBundle_proj_preimage, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, Bundle.contMDiffOn_proj, Bundle.contMDiff_proj, contMDiffAt_section_of_mem_baseSet, tangentMap_chart_symm, UniqueMDiffWithinAt.bundle_preimage, contMDiffAt_vectorSpace_iff_contDiffAt, Bundle.mdifferentiableWithinAt_zeroSection, mdifferentiable_addInvariantVectorField, Trivialization.mdifferentiableWithinAt_section_iff, Bundle.contMDiff_zeroSection, extChartAt_target, contMDiffAt_localFrame_of_mem, mdifferentiableAt_section, Bundle.mdifferentiable_proj, ContMDiffSection.contMDiff, contMDiff_equivTangentBundleProd, Trivialization.contMDiffWithinAt_iff, UniqueMDiffOn.bundle_preimage, Bundle.contMDiffAt_section, mdifferentiableAt_mulInvariantVectorField, Trivialization.mdifferentiableOn_section_iff, ContMDiffOn.contMDiffOn_tangentMapWithin, Trivialization.contMDiffAt_section_iff, IsLocalFrameOn.contMDiffOn_of_coeff, Trivialization.contMDiffOn_symm, Bundle.contMDiffAt_proj, Trivialization.contMDiffOn_iff, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, hom_chart, TangentBundle.coe_chartAt_symm_fst, Bundle.contMDiffWithinAt_section, Bundle.mdifferentiableOn_zeroSection, Trivialization.mdifferentiableWithinAt_totalSpace_iff, ContMDiffSection.mdifferentiable', contMDiff_tangentBundleModelSpaceHomeomorph_symm, ContMDiffSection.mdifferentiableAt, ContMDiffSection.mdifferentiable, Bundle.mdifferentiable_zeroSection, IsLocalFrameOn.mdifferentiableAt_of_coeff, TangentBundle.chartAt_toPartialEquiv, contMDiffOn_vectorSpace_iff_contDiffOn, ContMDiffSection.contMDiff_toFun, mdifferentiableWithinAt_hom_bundle, IsLocalFrameOn.contMDiffAt_of_coeff_aux, Trivialization.contMDiffOn, contMDiffOn_section_of_mem_baseSet₀, Bundle.mdifferentiableAt_zeroSection, Trivialization.mdifferentiable, contMDiff_snd_tangentBundle_modelSpace, contMDiffWithinAt_hom_bundle, Trivialization.contMDiffWithinAt_section, TangentBundle.mem_chart_source_iff, contMDiffOn_section_of_mem_baseSet
chartedSpace' 📖	CompOp	2 math math: chartedSpace'_chartAt, ContMDiffFiberwiseLinear.hasGroupoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chartedSpace'_chartAt 📖	mathematical	—	chartAt instTopologicalSpaceProd Bundle.TotalSpace chartedSpace' Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj trivializationAt	—	—
chartedSpace_chartAt 📖	mathematical	—	chartAt ModelProd instTopologicalSpaceModelProd Bundle.TotalSpace chartedSpace OpenPartialHomeomorph.trans instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj trivializationAt OpenPartialHomeomorph.prod OpenPartialHomeomorph.refl	—	Trivialization.coe_coe Trivialization.coe_fst' mem_baseSet_trivializationAt
chartedSpace_chartAt_symm_fst 📖	mathematical	ModelProd Set Set.instMembership PartialEquiv.target Bundle.TotalSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceModelProd chartAt chartedSpace	Bundle.TotalSpace.proj OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm	—	chartedSpace_chartAt Trivialization.proj_symm_apply
extChartAt 📖	mathematical	—	extChartAt Bundle.TotalSpace ModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf chartedSpace PartialEquiv.trans OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj trivializationAt PartialEquiv.prod PartialEquiv.refl	—	chartedSpace_chartAt PartialEquiv.trans_assoc PartialEquiv.prod_trans PartialEquiv.refl_trans
extChartAt_target 📖	mathematical	—	PartialEquiv.target Bundle.TotalSpace extChartAt ModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf chartedSpace SProd.sprod Set Set.instSProd Set.instInter Bundle.TotalSpace.proj Set.preimage PartialEquiv.toFun PartialEquiv.symm Trivialization.baseSet trivializationAt Set.univ	—	extChartAt PartialEquiv.trans_target Trivialization.target_eq Set.inter_prod
writtenInExtChartAt_trivializationAt 📖	mathematical	Set Set.instMembership PartialEquiv.target Bundle.TotalSpace extChartAt ModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf chartedSpace	writtenInExtChartAt instTopologicalSpaceProd prodChartedSpace chartedSpaceSelf Trivialization.toFun' Bundle.TotalSpace.proj trivializationAt	—	writtenInExtChartAt_chartAt_comp
writtenInExtChartAt_trivializationAt_symm 📖	mathematical	Set Set.instMembership PartialEquiv.target Bundle.TotalSpace extChartAt ModelProd Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf chartedSpace	writtenInExtChartAt instTopologicalSpaceProd prodChartedSpace chartedSpaceSelf Trivialization.toFun' Bundle.TotalSpace.proj trivializationAt OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm Trivialization.toOpenPartialHomeomorph	—	writtenInExtChartAt_chartAt_symm_comp

Trivialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_iff 📖	mathematical	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph Bundle.TotalSpace.proj	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace chartedSpaceSelf toFun'	—	contMDiffWithinAt_iff
contMDiffAt_section_iff 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace Bundle.TotalSpace.mk' chartedSpaceSelf toFun'	—	contMDiffWithinAt_section
contMDiffOn 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace instTopologicalSpaceProd prodChartedSpace chartedSpaceSelf toFun' Bundle.TotalSpace.proj PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv toOpenPartialHomeomorph	—	contMDiffOn_id ContMDiffOn.congr ContMDiffOn.prodMk contMDiffOn_iff Set.mapsTo_id mk_proj_snd
contMDiffOn_iff 📖	mathematical	Set.MapsTo Bundle.TotalSpace PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph Bundle.TotalSpace.proj	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace chartedSpaceSelf toFun'	—	contMDiffWithinAt_iff
contMDiffOn_section_baseSet_iff 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk' baseSet Bundle.TotalSpace.proj chartedSpaceSelf toFun'	—	contMDiffOn_section_iff open_baseSet subset_rfl Set.instReflSubset
contMDiffOn_section_iff 📖	mathematical	IsOpen Set Set.instHasSubset baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace Bundle.TotalSpace.mk' chartedSpaceSelf toFun'	—	ContMDiffWithinAt.contMDiffAt IsOpen.mem_nhds ContMDiffAt.contMDiffWithinAt contMDiffAt_section_iff
contMDiffOn_symm 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf instTopologicalSpaceProd prodChartedSpace chartedSpaceSelf Bundle.TotalSpace FiberBundle.chartedSpace OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.symm toOpenPartialHomeomorph Bundle.TotalSpace.proj PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	contMDiffOn_iff OpenPartialHomeomorph.symm_mapsTo ContMDiffOn.congr contMDiffOn_fst proj_symm_apply contMDiffOn_snd apply_symm_apply
contMDiffOn_symm_trans 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf instTopologicalSpaceProd prodChartedSpace chartedSpaceSelf OpenPartialHomeomorph.toFun' OpenPartialHomeomorph.trans Bundle.TotalSpace OpenPartialHomeomorph.symm toOpenPartialHomeomorph Bundle.TotalSpace.proj Set Set.instInter PartialEquiv.target OpenPartialHomeomorph.toPartialEquiv	—	mem_target ContMDiffOn.congr ContMDiffOn.prodMk contMDiffOn_fst ContMDiffOn.coordChange contMDiffOn_snd Set.mapsTo_inter symm_coe_proj coe_fst' proj_symm_apply
contMDiffWithinAt_iff 📖	mathematical	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph Bundle.TotalSpace.proj	ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace chartedSpaceSelf toFun'	—	Bundle.contMDiffWithinAt_totalSpace contMDiffWithinAt_snd_comp_iff₂ instMemTrivializationAtlasTrivializationAt FiberBundle.mem_trivializationAt_proj_source
contMDiffWithinAt_section 📖	mathematical	Set Set.instMembership baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContMDiffWithinAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace Bundle.TotalSpace.mk' chartedSpaceSelf toFun'	—	contMDiffWithinAt_iff mem_source
contMDiffWithinAt_snd_comp_iff₂ 📖	mathematical	ContMDiffWithinAt Bundle.TotalSpace Bundle.TotalSpace.proj Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph	modelWithCornersSelf chartedSpaceSelf toFun'	—	ContMDiffWithinAt.change_section_trivialization
contMDiff_iff 📖	mathematical	Bundle.TotalSpace Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup toOpenPartialHomeomorph Bundle.TotalSpace.proj	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace chartedSpaceSelf toFun'	—	contMDiffAt_iff

VectorBundleCore

Definitions

Name	Category	Theorems
IsContMDiff 📖	CompData	1 math math: tangentBundleCore.isContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffOn_coordChange 📖	mathematical	—	ContMDiffOn 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.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf coordChange Set Set.instInter baseSet	—	IsContMDiff.contMDiffOn_coordChange
instContMDiffVectorBundle 📖	mathematical	—	ContMDiffVectorBundle Fiber ESeminormedAddCommMonoid.toAddCommMonoid topologicalSpaceFiber ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid moduleFiber toTopologicalSpace fiberBundle vectorBundle	—	vectorBundle RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear ContMDiffOn.congr contMDiffOn_coordChange ContinuousLinearMap.ext localTriv_coordChange_eq

VectorBundleCore.IsContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffOn_coordChange 📖	mathematical	—	ContMDiffOn 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.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf VectorBundleCore.coordChange Set Set.instInter VectorBundleCore.baseSet	—	—

VectorPrebundle

Definitions

Name	Category	Theorems
IsContMDiff 📖	CompData	1 math math: Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff
contMDiffCoordChange 📖	CompOp	3 math math: mk_contMDiffCoordChange, contMDiffOn_contMDiffCoordChange, contMDiffCoordChange_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffCoordChange_apply 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas Set.instInter Pretrivialization.baseSet	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 contMDiffCoordChange Pretrivialization.toFun' Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup IsContMDiff.exists_contMDiffCoordChange
contMDiffOn_contMDiffCoordChange 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas	ContMDiffOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf contMDiffCoordChange Set.instInter Pretrivialization.baseSet	—	RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup IsContMDiff.exists_contMDiffCoordChange
contMDiffVectorBundle 📖	mathematical	—	ContMDiffVectorBundle totalSpaceTopology toFiberBundle toVectorBundle	—	toVectorBundle RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear ContMDiffOn.congr contMDiffOn_contMDiffCoordChange ContinuousLinearMap.ext contMDiffCoordChange_apply ContinuousLinearEquiv.coe_coe Trivialization.coordChangeL_apply
mk_contMDiffCoordChange 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership pretrivializationAtlas Set.instInter Pretrivialization.baseSet	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 contMDiffCoordChange Pretrivialization.toFun' Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Pretrivialization.mk_symm Pretrivialization.coe_fst' Pretrivialization.proj_symm_apply' contMDiffCoordChange_apply

VectorPrebundle.IsContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_contMDiffCoordChange 📖	mathematical	Pretrivialization Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj Set Set.instMembership VectorPrebundle.pretrivializationAtlas	ContMDiffOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf Set.instInter Pretrivialization.baseSet DFunLike.coe ContinuousLinearMap.funLike Pretrivialization.toFun' Pretrivialization.symm AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	—

(root)

Definitions

Name	Category	Theorems
ContMDiffVectorBundle 📖	CompData	15 math math: instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, ContMDiffVectorBundle.pullback, instContMDiffVectorBundleOfTopWithTopENat, ContMDiffVectorBundle.continuousLinearMap, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, instContMDiffVectorBundleOfNatWithTopENat, VectorBundleCore.instContMDiffVectorBundle, VectorPrebundle.contMDiffVectorBundle, TangentBundle.contMDiffVectorBundle, instContMDiffVectorBundleOfNatWithTopENat_1, instContMDiffVectorBundleOfSomeENatTopOfLEInfty, Bundle.Trivial.contMDiffVectorBundle, ContMDiffVectorBundle.of_le, Bundle.Prod.contMDiffVectorBundle, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiffAt_coordChangeL 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContMDiffAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear	—	ContMDiffOn.contMDiffAt RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear contMDiffOn_coordChangeL IsOpen.mem_nhds IsOpen.inter Trivialization.open_baseSet
contMDiffAt_section_of_mem_baseSet 📖	mathematical	Set Set.instMembership Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContMDiffAt Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace Bundle.TotalSpace.mk' chartedSpaceSelf Trivialization.toFun'	—	Trivialization.contMDiffAt_section_iff
contMDiffOn_coordChangeL 📖	mathematical	—	ContMDiffOn 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.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids Trivialization.coordChangeL trivialization_linear Set Set.instInter Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	ContMDiffVectorBundle.contMDiffOn_coordChangeL
contMDiffOn_section_of_mem_baseSet 📖	mathematical	IsOpen Set Set.instHasSubset Trivialization.baseSet Bundle.TotalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf FiberBundle.chartedSpace Bundle.TotalSpace.mk' chartedSpaceSelf Trivialization.toFun'	—	Trivialization.contMDiffOn_section_iff
contMDiffOn_section_of_mem_baseSet₀ 📖	mathematical	—	ContMDiffOn Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace Bundle.TotalSpace.mk' Trivialization.baseSet Bundle.TotalSpace.proj chartedSpaceSelf Trivialization.toFun'	—	Trivialization.contMDiffOn_section_baseSet_iff
contMDiffOn_symm_coordChangeL 📖	mathematical	—	ContMDiffOn 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.toNormedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ContinuousLinearMap.toNormedSpace smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing modelWithCornersSelf ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup chartedSpaceSelf ContinuousLinearEquiv.toContinuousLinearMap RingHomInvPair.ids ContinuousLinearEquiv.symm Trivialization.coordChangeL trivialization_linear Set Set.instInter Trivialization.baseSet Bundle.TotalSpace Bundle.TotalSpace.proj	—	RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear Set.inter_comm ContMDiffOn.congr ContMDiffVectorBundle.contMDiffOn_coordChangeL Trivialization.symm_coordChangeL
instContMDiffVectorBundleOfNatWithTopENat 📖	mathematical	—	ContMDiffVectorBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Nat.instAtLeastTwoHAddOfNat ContMDiffVectorBundle.of_le one_le_two WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
instContMDiffVectorBundleOfNatWithTopENat_1 📖	mathematical	—	ContMDiffVectorBundle WithTop ENat WithTop.zero instZeroENat	—	RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.ids trivialization_linear contMDiffOn_zero_iff VectorBundle.continuousOn_coordChange'
instContMDiffVectorBundleOfSomeENatTopOfLEInfty 📖	mathematical	—	ContMDiffVectorBundle	—	ContMDiffVectorBundle.of_le ENat.LEInfty.out
instContMDiffVectorBundleOfTopWithTopENat 📖	mathematical	—	ContMDiffVectorBundle	—	ContMDiffVectorBundle.of_le le_top

---

← Back to Index