Tangent

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

Statistics

Metric	Count
Definitions fiberBundle, inTangentCoordinates, instTopologicalSpaceTangentBundle, tangentBundleCore, tangentBundleModelSpaceHomeomorph, tangentCoordChange	6
Theorems chartAt, chartAt_toPartialEquiv, coe_chartAt_fst, coe_chartAt_symm_fst, contMDiffVectorBundle, continuousLinearMapAt_model_space, continuousLinearMapAt_trivializationAt_eq_core, coordChange_model_space, mem_chart_source_iff, mem_chart_target_iff, symmL_model_space, symmL_trivializationAt_eq_core, trivializationAt_apply, trivializationAt_baseSet, trivializationAt_eq_localTriv, trivializationAt_fst, trivializationAt_source, trivializationAt_target, vectorBundle, contDiffOn_fderiv_coord_change, contMDiffAt_vectorSpace_iff_contDiffAt, contMDiffOn_vectorSpace_iff_contDiffOn, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, contMDiff_snd_tangentBundle_modelSpace, contMDiff_tangentBundleModelSpaceHomeomorph, contMDiff_tangentBundleModelSpaceHomeomorph_symm, contMDiff_vectorSpace_iff_contDiff, continuousOn_tangentCoordChange, hasFDerivWithinAt_tangentCoordChange, inCoordinates_tangent_bundle_core_model_space, inTangentCoordinates_eq, inTangentCoordinates_model_space, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, isContMDiff, tangentBundleCore_baseSet, tangentBundleCore_coordChange, tangentBundleCore_coordChange_achart, tangentBundleCore_coordChange_model_space, tangentBundleCore_indexAt, tangentBundleCore_localTriv_baseSet, tangentBundleModelSpaceHomeomorph_coe, tangentBundleModelSpaceHomeomorph_coe_symm, tangentBundle_model_space_chartAt, tangentBundle_model_space_coe_chartAt, tangentBundle_model_space_coe_chartAt_symm, tangentCoordChange_comp, tangentCoordChange_def, tangentCoordChange_self, trivializationAt_model_space_apply	51
Total	57

TangentBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
chartAt 📖	mathematical	—	chartAt ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TangentBundle instTopologicalSpaceTangentBundle FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle OpenPartialHomeomorph.trans FiberBundleCore.TotalSpace Set.Elem OpenPartialHomeomorph atlas VectorBundleCore.toFiberBundleCore tangentBundleCore FiberBundleCore.toTopologicalSpace instTopologicalSpaceProd Bundle.Trivialization.toOpenPartialHomeomorph FiberBundleCore.proj FiberBundleCore.localTriv achart Bundle.TotalSpace.proj OpenPartialHomeomorph.prod OpenPartialHomeomorph.refl	—	—
chartAt_toPartialEquiv 📖	mathematical	—	OpenPartialHomeomorph.toPartialEquiv TangentBundle ModelProd instTopologicalSpaceTangentBundle instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup chartAt FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle PartialEquiv.trans FiberBundleCore.TotalSpace Set.Elem OpenPartialHomeomorph atlas VectorBundleCore.toFiberBundleCore tangentBundleCore FiberBundleCore.localTrivAsPartialEquiv achart Bundle.TotalSpace.proj PartialEquiv.prod PartialEquiv.refl	—	—
coe_chartAt_fst 📖	mathematical	—	OpenPartialHomeomorph.toFun' TangentBundle ModelProd instTopologicalSpaceTangentBundle instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup chartAt FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.proj	—	—
coe_chartAt_symm_fst 📖	mathematical	—	Bundle.TotalSpace.proj TangentSpace OpenPartialHomeomorph.toFun' ModelProd TangentBundle instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceTangentBundle OpenPartialHomeomorph.symm chartAt FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	—	—
contMDiffVectorBundle 📖	mathematical	—	ContMDiffVectorBundle TangentSpace ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle IsManifold.of_le WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat WithTop.add instAddENat le_add_self Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.canonicallyOrderedAdd instCanonicallyOrderedAddENat TangentSpace.fiberBundle TangentSpace.vectorBundle	—	IsManifold.of_le le_add_self WithTop.canonicallyOrderedAdd tangentBundleCore.isContMDiff VectorBundleCore.instContMDiffVectorBundle
continuousLinearMapAt_model_space 📖	mathematical	—	Bundle.Trivialization.continuousLinearMapAt TangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top TangentSpace.fiberBundle FiberBundle.trivializationAt trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule ContinuousLinearMap.one	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt continuousLinearMapAt_trivializationAt_eq_core Set.mem_univ coordChange_model_space
continuousLinearMapAt_trivializationAt_eq_core 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	Bundle.Trivialization.continuousLinearMapAt TangentSpace ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle TangentSpace.fiberBundle FiberBundle.trivializationAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt VectorBundleCore.coordChange Set.Elem OpenPartialHomeomorph atlas tangentBundleCore achart	—	trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt VectorBundleCore.trivializationAt_continuousLinearMapAt
coordChange_model_space 📖	mathematical	—	VectorBundleCore.coordChange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Set.Elem OpenPartialHomeomorph atlas chartedSpaceSelf tangentBundleCore modelWithCornersSelf IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top achart ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.one	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace PartialEquiv.trans_refl Set.range_id fderivWithin_id IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace uniqueDiffWithinAt_univ NormedField.nhdsNE_neBot
mem_chart_source_iff 📖	mathematical	—	TangentBundle Set Set.instMembership PartialEquiv.source ModelProd OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceTangentBundle instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup chartAt FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.proj	—	FiberBundle.chartedSpace_chartAt
mem_chart_target_iff 📖	mathematical	—	Set ModelProd Set.instMembership PartialEquiv.target TangentBundle OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceTangentBundle instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup chartAt FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.proj	—	FiberBundle.chartedSpace_chartAt PartialEquiv.prod_symm
symmL_model_space 📖	mathematical	—	Bundle.Trivialization.symmL TangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top TangentSpace.fiberBundle FiberBundle.trivializationAt trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule ContinuousLinearMap.one	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt symmL_trivializationAt_eq_core Set.mem_univ coordChange_model_space
symmL_trivializationAt_eq_core 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	Bundle.Trivialization.symmL TangentSpace ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle TangentSpace.fiberBundle FiberBundle.trivializationAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt VectorBundleCore.coordChange Set.Elem OpenPartialHomeomorph atlas tangentBundleCore achart	—	trivialization_linear TangentSpace.vectorBundle instMemTrivializationAtlasTrivializationAt VectorBundleCore.trivializationAt_symmL
trivializationAt_apply 📖	mathematical	—	Bundle.Trivialization.toFun' Bundle.TotalSpace TangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj instTopologicalSpaceTangentBundle FiberBundle.trivializationAt instTopologicalSpaceTangentSpace TangentSpace.fiberBundle DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike fderivWithin PartialEquiv.toFun OpenPartialHomeomorph.extend chartAt PartialEquiv.symm Set.range ModelWithCorners.toFun' Bundle.TotalSpace.snd	—	—
trivializationAt_baseSet 📖	mathematical	—	Bundle.Trivialization.baseSet Bundle.TotalSpace TangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceTangentBundle Bundle.TotalSpace.proj FiberBundle.trivializationAt instTopologicalSpaceTangentSpace TangentSpace.fiberBundle PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	—	—
trivializationAt_eq_localTriv 📖	mathematical	—	FiberBundle.trivializationAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup TangentSpace instTopologicalSpaceTangentBundle instTopologicalSpaceTangentSpace TangentSpace.fiberBundle FiberBundleCore.localTriv Set.Elem OpenPartialHomeomorph atlas VectorBundleCore.toFiberBundleCore tangentBundleCore achart	—	—
trivializationAt_fst 📖	mathematical	—	Bundle.Trivialization.toFun' Bundle.TotalSpace TangentSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj instTopologicalSpaceTangentBundle FiberBundle.trivializationAt instTopologicalSpaceTangentSpace TangentSpace.fiberBundle	—	—
trivializationAt_source 📖	mathematical	—	PartialEquiv.source Bundle.TotalSpace TangentSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceTangentBundle instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj FiberBundle.trivializationAt instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Set.preimage chartAt	—	—
trivializationAt_target 📖	mathematical	—	PartialEquiv.target Bundle.TotalSpace TangentSpace OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceTangentBundle instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.Trivialization.toOpenPartialHomeomorph Bundle.TotalSpace.proj FiberBundle.trivializationAt instTopologicalSpaceTangentSpace TangentSpace.fiberBundle SProd.sprod Set Set.instSProd PartialEquiv.source chartAt Set.univ	—	—

TangentSpace

Definitions

Name	Category	Theorems
fiberBundle 📖	CompOp	86 math math: TangentBundle.continuousLinearMapAt_model_space, TangentBundle.tangentMap_tangentBundle_pure, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffOn.mlieBracketWithin_vectorField, ContMDiffWithinAt.mlieBracketWithin_vectorField, tangentMap_chart, TangentBundle.symmL_trivializationAt, contMDiff_addInvariantVectorField, TangentBundle.coe_chartAt_fst, contMDiff_mulInvariantVectorField, contMDiff_equivTangentBundleProd_symm, TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, tangentBundle_model_space_coe_chartAt, contMDiffAt_mulInvariantVectorField, mdifferentiableAt_addInvariantVectorField, ContMDiff.contMDiff_tangentMap, MDifferentiableAt.mpullback_vectorField, TangentBundle.trivializationAt_fst, CovariantDerivative.torsion_apply, mdifferentiable_mulInvariantVectorField, ContMDiffWithinAt.mpullbackWithin_vectorField_inter, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, TangentBundle.trivializationAt_apply, contMDiff_vectorSpace_iff_contDiff, ContMDiffOn.mpullbackWithin_vectorField_inter, MDifferentiable.mpullback_vectorField, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq, ContMDiffWithinAt.mpullback_vectorField_preimage, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq, ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq, trivializationAt_model_space_apply, TangentBundle.trivializationAt_source, ContMDiffWithinAt.mpullbackWithin_vectorField', tangentBundle_model_space_coe_chartAt_symm, TangentBundle.chartAt, ContMDiffAt.mlieBracket_vectorField, TangentBundle.contMDiffVectorBundle, UniqueMDiffOn.tangentBundle_proj_preimage, TangentBundle.continuousLinearMapAt_trivializationAt, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, CovariantDerivative.torsion_eq_zero_iff, MDifferentiableOn.mpullback_vectorField_preimage, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq, tangentMap_chart_symm, contMDiffAt_vectorSpace_iff_contDiffAt, TangentBundle.trivializationAt_eq_localTriv, mdifferentiable_addInvariantVectorField, vectorBundle, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, TangentBundle.symmL_model_space, ContDiff.mlieBracket_vectorField, MDifferentiableWithinAt.mpullback_vectorField_preimage, contMDiff_equivTangentBundleProd, MDifferentiableOn.mpullbackWithin_vectorField_inter, ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq, TangentBundle.trivializationAt_baseSet, mdifferentiableAt_mulInvariantVectorField, ContMDiffCovariantDerivativeOn.contMDiff, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter, ContMDiffOn.contMDiffOn_tangentMapWithin, ContMDiffOn.mpullback_vectorField_preimage, IsCovariantDerivativeOn.torsion_apply_eq_extend, MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq, ContMDiffWithinAt.mpullbackWithin_vectorField, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, ContMDiffAt.mpullback_vectorField_preimage, TangentBundle.coe_chartAt_symm_fst, contMDiff_tangentBundleModelSpaceHomeomorph_symm, CovariantDerivative.torsion_apply_eq_extend, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, TangentBundle.chartAt_toPartialEquiv, contMDiffOn_vectorSpace_iff_contDiffOn, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold, inCoordinates_tangent_bundle_core_model_space, contMDiff_snd_tangentBundle_modelSpace, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq', ContMDiff.mpullback_vectorField, TangentBundle.mem_chart_source_iff, TangentBundle.trivializationAt_target, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
vectorBundle 📖	mathematical	—	VectorBundle TangentSpace ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle fiberBundle	—	VectorBundleCore.vectorBundle

(root)

Definitions

Name	Category	Theorems
inTangentCoordinates 📖	CompOp	9 math math: ContMDiffWithinAt.mfderivWithin_const, inTangentCoordinates_eq_mfderiv_comp, ContMDiffAt.mfderiv_apply, ContMDiffAt.mfderiv_const, inTangentCoordinates_eq, ContMDiffWithinAt.mfderivWithin, ContMDiffWithinAt.mfderivWithin_apply, ContMDiffAt.mfderiv, inTangentCoordinates_model_space
instTopologicalSpaceTangentBundle 📖	CompOp	90 math math: TangentBundle.continuousLinearMapAt_model_space, TangentBundle.tangentMap_tangentBundle_pure, instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold, contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt, ContMDiffOn.mlieBracketWithin_vectorField, ContMDiffWithinAt.mlieBracketWithin_vectorField, tangentMap_chart, TangentBundle.symmL_trivializationAt, contMDiff_addInvariantVectorField, TangentBundle.coe_chartAt_fst, contMDiff_mulInvariantVectorField, contMDiff_equivTangentBundleProd_symm, TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, tangentBundle_model_space_coe_chartAt, contMDiffAt_mulInvariantVectorField, mdifferentiableAt_addInvariantVectorField, ContMDiff.contMDiff_tangentMap, MDifferentiableAt.mpullback_vectorField, TangentBundle.trivializationAt_fst, CovariantDerivative.torsion_apply, mdifferentiable_mulInvariantVectorField, ContMDiffWithinAt.mpullbackWithin_vectorField_inter, instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold, TangentBundle.trivializationAt_apply, contMDiff_vectorSpace_iff_contDiff, ContMDiffOn.mpullbackWithin_vectorField_inter, MDifferentiable.mpullback_vectorField, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq, ContMDiffWithinAt.mpullback_vectorField_preimage, ContMDiffOn.continuousOn_tangentMapWithin, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq, ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq, trivializationAt_model_space_apply, TangentBundle.trivializationAt_source, ContMDiffWithinAt.mpullbackWithin_vectorField', tangentBundle_model_space_coe_chartAt_symm, tangentBundleModelSpaceHomeomorph_coe, TangentBundle.chartAt, ContMDiffAt.mlieBracket_vectorField, TangentBundle.contMDiffVectorBundle, UniqueMDiffOn.tangentBundle_proj_preimage, TangentBundle.continuousLinearMapAt_trivializationAt, tangentBundle_model_space_chartAt, TangentBundle.mem_chart_target_iff, CovariantDerivative.torsion_eq_zero_iff, MDifferentiableOn.mpullback_vectorField_preimage, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq, tangentMap_chart_symm, contMDiffAt_vectorSpace_iff_contDiffAt, TangentBundle.trivializationAt_eq_localTriv, mdifferentiable_addInvariantVectorField, TangentSpace.vectorBundle, VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm, TangentBundle.symmL_model_space, ContDiff.mlieBracket_vectorField, tangentBundleModelSpaceHomeomorph_coe_symm, MDifferentiableWithinAt.mpullback_vectorField_preimage, contMDiff_equivTangentBundleProd, MDifferentiableOn.mpullbackWithin_vectorField_inter, ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq, TangentBundle.trivializationAt_baseSet, mdifferentiableAt_mulInvariantVectorField, ContMDiffCovariantDerivativeOn.contMDiff, MDifferentiableWithinAt.mpullbackWithin_vectorField_inter, ContMDiffOn.contMDiffOn_tangentMapWithin, ContMDiffOn.mpullback_vectorField_preimage, IsCovariantDerivativeOn.torsion_apply_eq_extend, MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq, ContMDiffWithinAt.mpullbackWithin_vectorField, contMDiffAt_addInvariantVectorField, contMDiff_tangentBundleModelSpaceHomeomorph, ContMDiffAt.mpullback_vectorField_preimage, TangentBundle.coe_chartAt_symm_fst, contMDiff_tangentBundleModelSpaceHomeomorph_symm, CovariantDerivative.torsion_apply_eq_extend, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq, ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem, VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm, TangentBundle.chartAt_toPartialEquiv, contMDiffOn_vectorSpace_iff_contDiffOn, ContMDiff.continuous_tangentMap, instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold, inCoordinates_tangent_bundle_core_model_space, contMDiff_snd_tangentBundle_modelSpace, ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq', ContMDiff.mpullback_vectorField, TangentBundle.mem_chart_source_iff, TangentBundle.trivializationAt_target, ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin
tangentBundleCore 📖	CompOp	14 math math: TangentBundle.symmL_trivializationAt_eq_core, TangentBundle.continuousLinearMapAt_trivializationAt_eq_core, TangentBundle.coordChange_model_space, inTangentCoordinates_eq, TangentBundle.chartAt, tangentBundleCore_coordChange_model_space, tangentBundleCore_coordChange, tangentBundleCore.isContMDiff, TangentBundle.trivializationAt_eq_localTriv, tangentBundleCore_baseSet, tangentBundleCore_localTriv_baseSet, TangentBundle.chartAt_toPartialEquiv, tangentBundleCore_indexAt, tangentBundleCore_coordChange_achart
tangentBundleModelSpaceHomeomorph 📖	CompOp	4 math math: tangentBundleModelSpaceHomeomorph_coe, tangentBundleModelSpaceHomeomorph_coe_symm, contMDiff_tangentBundleModelSpaceHomeomorph, contMDiff_tangentBundleModelSpaceHomeomorph_symm
tangentCoordChange 📖	CompOp	8 math math: tangentCoordChange_def, IsMIntegralCurveOn.hasDerivWithinAt, continuousOn_tangentCoordChange, mfderiv_chartAt_eq_tangentCoordChange, tangentCoordChange_comp, hasFDerivWithinAt_tangentCoordChange, tangentCoordChange_self, IsMIntegralCurveAt.eventually_hasDerivAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_fderiv_coord_change 📖	mathematical	—	ContDiffOn ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup 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 ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing fderivWithin PartialEquiv.toFun OpenPartialHomeomorph.extend OpenPartialHomeomorph Set Set.instMembership atlas PartialEquiv.symm Set.range ModelWithCorners.toFun' PartialEquiv.source PartialEquiv.trans	—	Eq.trans_subset ModelWithCorners.extendCoordChange_source Set.image_subset_range ContDiffWithinAt.mono RingHomIsometric.ids smulCommClass_self ContDiffWithinAt.fderivWithin_right ContDiffWithinAt.mono_of_mem_nhdsWithin ModelWithCorners.contDiffOn_extendCoordChange IsManifold.subset_maximalAtlas ModelWithCorners.extendCoordChange_source_mem_nhdsWithin ModelWithCorners.uniqueDiffOn le_rfl
contMDiffAt_vectorSpace_iff_contDiffAt 📖	mathematical	—	ContMDiffAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.mk' ContDiffAt	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace
contMDiffOn_vectorSpace_iff_contDiffOn 📖	mathematical	—	ContMDiffOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.mk' ContDiffOn	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace
contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt 📖	mathematical	—	ContMDiffWithinAt UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.mk' ContDiffWithinAt	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace ContMDiffWithinAt.contDiffWithinAt ContMDiffAt.comp_contMDiffWithinAt ContMDiff.contMDiffAt contMDiff_snd_tangentBundle_modelSpace Bundle.contMDiffWithinAt_totalSpace contMDiffWithinAt_id trivializationAt_model_space_apply ContDiffWithinAt.contMDiffWithinAt
contMDiff_snd_tangentBundle_modelSpace 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent TangentBundle chartedSpaceSelf instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle modelWithCornersSelf Bundle.TotalSpace.snd	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace ContMDiff.comp chartedSpaceSelf_prod contMDiff_snd contMDiff_tangentBundleModelSpaceHomeomorph
contMDiff_tangentBundleModelSpaceHomeomorph 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.tangent TangentBundle chartedSpaceSelf instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle ModelWithCorners.prod modelWithCornersSelf DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike tangentBundleModelSpaceHomeomorph	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace contMDiff_iff Bundle.TotalSpace.isManifold TangentSpace.vectorBundle instContMDiffVectorBundleOfTopWithTopENat instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold Homeomorph.continuous ContDiffOn.congr contDiffOn_id tangentBundle_model_space_chartAt ModelWithCorners.target_eq Set.inter_univ PartialEquiv.refl_trans ModelWithCorners.source_eq Set.univ_prod_univ ModelWithCorners.left_inv
contMDiff_tangentBundleModelSpaceHomeomorph_symm 📖	mathematical	—	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf chartedSpaceSelf ModelWithCorners.tangent TangentBundle instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm tangentBundleModelSpaceHomeomorph	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace contMDiff_iff Bundle.TotalSpace.isManifold TangentSpace.vectorBundle instContMDiffVectorBundleOfTopWithTopENat instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold Homeomorph.continuous ContDiffOn.congr contDiffOn_id PartialEquiv.refl_trans ModelWithCorners.target_eq tangentBundle_model_space_chartAt ModelWithCorners.source_eq Set.univ_prod_univ Set.inter_univ ModelWithCorners.left_inv
contMDiff_vectorSpace_iff_contDiff 📖	mathematical	—	ContMDiff UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup modelWithCornersSelf chartedSpaceSelf Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod Bundle.TotalSpace TangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.chartedSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.mk' ContDiff	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace
continuousOn_tangentCoordChange 📖	mathematical	—	ContinuousOn 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.topologicalSpace NormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup tangentCoordChange Set Set.instInter PartialEquiv.source extChartAt	—	SeminormedAddCommGroup.toIsTopologicalAddGroup extChartAt_source VectorBundleCore.continuousOn_coordChange
hasFDerivWithinAt_tangentCoordChange 📖	mathematical	Set Set.instMembership Set.instInter PartialEquiv.source extChartAt	HasFDerivWithinAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialEquiv.toFun extChartAt PartialEquiv.symm tangentCoordChange Set.range ModelWithCorners.toFun'	—	PartialEquiv.trans_source'' PartialEquiv.symm_symm PartialEquiv.symm_target Set.mem_image_of_mem DifferentiableWithinAt.hasFDerivWithinAt ContDiffWithinAt.differentiableWithinAt contDiffWithinAt_ext_coord_change one_ne_zero NeZero.charZero_one WithTop.charZero
inCoordinates_tangent_bundle_core_model_space 📖	mathematical	—	ContinuousLinearMap.inCoordinates TangentSpace chartedSpaceSelf ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid RingHom.id Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField instModuleTangentSpace instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top TangentSpace.fiberBundle TangentSpace.vectorBundle	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace TangentSpace.vectorBundle RingHomCompTriple.right_ids RingHomCompTriple.ids VectorBundleCore.vectorBundle VectorBundleCore.inCoordinates_eq ContinuousLinearMap.comp.congr_simp tangentBundleCore_coordChange_model_space ContinuousLinearMap.id_comp ContinuousLinearMap.comp_id
inTangentCoordinates_eq 📖	mathematical	Set Set.instMembership PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv chartAt	inTangentCoordinates ContinuousLinearMap.comp 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 RingHomCompTriple.ids VectorBundleCore.coordChange Set.Elem OpenPartialHomeomorph atlas tangentBundleCore achart	—	VectorBundleCore.inCoordinates_eq
inTangentCoordinates_model_space 📖	mathematical	—	inTangentCoordinates chartedSpaceSelf IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace TangentSpace.vectorBundle inCoordinates_tangent_bundle_core_model_space
instContMDiffVectorBundleOfNatWithTopENatTangentSpaceOfIsManifold 📖	mathematical	—	ContMDiffVectorBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat TangentSpace ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle TangentSpace.fiberBundle TangentSpace.vectorBundle	—	Nat.instAtLeastTwoHAddOfNat TangentBundle.contMDiffVectorBundle
instContMDiffVectorBundleSomeENatTopTangentSpaceOfIsManifold 📖	mathematical	—	ContMDiffVectorBundle WithTop.some ENat Top.top instTopENat TangentSpace ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle TangentSpace.fiberBundle TangentSpace.vectorBundle	—	TangentBundle.contMDiffVectorBundle
instContMDiffVectorBundleTopWithTopENatTangentSpaceOfIsManifold 📖	mathematical	—	ContMDiffVectorBundle Top.top WithTop ENat WithTop.top TangentSpace ESeminormedAddCommMonoid.toAddCommMonoid instTopologicalSpaceTangentSpace ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace instTopologicalSpaceTangentBundle TangentSpace.fiberBundle TangentSpace.vectorBundle	—	TangentBundle.contMDiffVectorBundle IsManifold.instOfTopWithTopENat
tangentBundleCore_baseSet 📖	mathematical	—	VectorBundleCore.baseSet Set.Elem OpenPartialHomeomorph atlas tangentBundleCore PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set Set.instMembership	—	—
tangentBundleCore_coordChange 📖	mathematical	—	VectorBundleCore.coordChange Set.Elem OpenPartialHomeomorph atlas tangentBundleCore fderivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialEquiv.toFun OpenPartialHomeomorph.extend Set Set.instMembership PartialEquiv.symm Set.range ModelWithCorners.toFun'	—	—
tangentBundleCore_coordChange_achart 📖	mathematical	—	VectorBundleCore.coordChange Set.Elem OpenPartialHomeomorph atlas tangentBundleCore achart fderivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialEquiv.toFun extChartAt PartialEquiv.symm Set.range ModelWithCorners.toFun'	—	—
tangentBundleCore_coordChange_model_space 📖	mathematical	—	VectorBundleCore.coordChange Set.Elem OpenPartialHomeomorph atlas chartedSpaceSelf tangentBundleCore IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top achart ContinuousLinearMap.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule	—	ContinuousLinearMap.ext IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace VectorBundleCore.coordChange_self Set.mem_univ
tangentBundleCore_indexAt 📖	mathematical	—	VectorBundleCore.indexAt Set.Elem OpenPartialHomeomorph atlas tangentBundleCore achart	—	—
tangentBundleCore_localTriv_baseSet 📖	mathematical	—	Bundle.Trivialization.baseSet Bundle.TotalSpace VectorBundleCore.Fiber Set.Elem OpenPartialHomeomorph atlas tangentBundleCore UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup VectorBundleCore.toTopologicalSpace Bundle.TotalSpace.proj VectorBundleCore.localTriv PartialEquiv.source OpenPartialHomeomorph.toPartialEquiv Set Set.instMembership	—	—
tangentBundleModelSpaceHomeomorph_coe 📖	mathematical	—	DFunLike.coe Homeomorph TangentBundle chartedSpaceSelf ModelProd instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup EquivLike.toFunLike Homeomorph.instEquivLike tangentBundleModelSpaceHomeomorph Equiv Bundle.TotalSpace Equiv.instEquivLike Bundle.TotalSpace.toProd	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace
tangentBundleModelSpaceHomeomorph_coe_symm 📖	mathematical	—	DFunLike.coe Homeomorph ModelProd TangentBundle chartedSpaceSelf instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm tangentBundleModelSpaceHomeomorph Equiv Bundle.TotalSpace Equiv.instEquivLike Equiv.symm Bundle.TotalSpace.toProd	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace
tangentBundle_model_space_chartAt 📖	mathematical	—	OpenPartialHomeomorph.toPartialEquiv TangentBundle chartedSpaceSelf ModelProd instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup chartAt FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Equiv.toPartialEquiv Bundle.TotalSpace Bundle.TotalSpace.toProd	—	PartialEquiv.ext IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace ModelProd.ext VectorBundleCore.coordChange_self mem_achart_source Bundle.TotalSpace.ext FiberBundleCore.open_source' Set.univ_prod_univ PartialEquiv.refl_prod_refl PartialEquiv.trans_refl
tangentBundle_model_space_coe_chartAt 📖	mathematical	—	OpenPartialHomeomorph.toFun' TangentBundle chartedSpaceSelf ModelProd instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup chartAt FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle DFunLike.coe Equiv Bundle.TotalSpace EquivLike.toFunLike Equiv.instEquivLike Bundle.TotalSpace.toProd	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace OpenPartialHomeomorph.coe_coe tangentBundle_model_space_chartAt
tangentBundle_model_space_coe_chartAt_symm 📖	mathematical	—	OpenPartialHomeomorph.toFun' ModelProd TangentBundle chartedSpaceSelf instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top OpenPartialHomeomorph.symm chartAt FiberBundle.chartedSpace TangentSpace instTopologicalSpaceTangentSpace TangentSpace.fiberBundle DFunLike.coe Equiv Bundle.TotalSpace EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Bundle.TotalSpace.toProd	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace OpenPartialHomeomorph.coe_coe OpenPartialHomeomorph.symm_toPartialEquiv tangentBundle_model_space_chartAt
tangentCoordChange_comp 📖	mathematical	Set Set.instMembership Set.instInter PartialEquiv.source extChartAt	DFunLike.coe 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.funLike tangentCoordChange	—	VectorBundleCore.coordChange_comp extChartAt_source
tangentCoordChange_def 📖	mathematical	—	tangentCoordChange fderivWithin NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace PartialEquiv.toFun extChartAt PartialEquiv.symm Set.range ModelWithCorners.toFun'	—	—
tangentCoordChange_self 📖	mathematical	Set Set.instMembership PartialEquiv.source extChartAt	DFunLike.coe 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.funLike tangentCoordChange	—	VectorBundleCore.coordChange_self tangentBundleCore_baseSet coe_achart extChartAt_source
trivializationAt_model_space_apply 📖	mathematical	—	Bundle.Trivialization.toFun' Bundle.TotalSpace TangentSpace chartedSpaceSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Bundle.TotalSpace.proj instTopologicalSpaceTangentBundle IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace Top.top WithTop.top FiberBundle.trivializationAt instTopologicalSpaceTangentSpace TangentSpace.fiberBundle Bundle.TotalSpace.snd	—	IsManifold.instOfNatWithTopENat_1 IsManifold.instOfNatWithTopENat_2 IsManifold.instOfTopWithTopENat Nat.instAtLeastTwoHAddOfNat instIsManifoldModelSpace fderivWithin_congr' ModelWithCorners.right_inv Set.mem_range_self PartialEquiv.refl_trans fderivWithin_id IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace ModelWithCorners.uniqueDiffWithinAt_image

tangentBundleCore

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isContMDiff 📖	mathematical	—	VectorBundleCore.IsContMDiff Set.Elem OpenPartialHomeomorph atlas tangentBundleCore IsManifold.of_le WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat WithTop.add instAddENat le_add_self Preorder.toLE WithTop.instPreorder instPreorderENat WithTop.canonicallyOrderedAdd instCanonicallyOrderedAddENat	—	IsManifold.of_le le_self_add WithTop.canonicallyOrderedAdd le_add_self RingHomIsometric.ids smulCommClass_self SeminormedAddCommGroup.toIsTopologicalAddGroup contMDiffOn_iff_source_of_mem_maximalAtlas IsManifold.subset_maximalAtlas Set.inter_subset_left contMDiffOn_iff_contDiffOn ContDiffOn.mono ContDiffOn.congr contDiffOn_fderiv_coord_change PartialEquiv.right_inv PartialEquiv.trans_source' Eq.subset Set.instReflSubset OpenPartialHomeomorph.extend_image_source_inter

---

← Back to Index