Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `ContMDiffVectorBundle`, `chartedSpace`, `chartedSpace'`, `IsContMDiff`, `IsContMDiff`, `contMDiffCoordChange`	6
Theorems `contMDiffVectorBundle`, `isManifold`, `contMDiffVectorBundle`, `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`, `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`, `contMDiffOn_coordChange`, `contMDiffOn_coordChange`, `instContMDiffVectorBundle`, `exists_contMDiffCoordChange`, `contMDiffCoordChange_apply`, `contMDiffOn_contMDiffCoordChange`, `contMDiffVectorBundle`, `mk_contMDiffCoordChange`, `contMDiffAt_coordChangeL`, `contMDiffOn_coordChangeL`, `contMDiffOn_symm_coordChangeL`, `instContMDiffVectorBundleOfNatWithTopENat`, `instContMDiffVectorBundleOfNatWithTopENat_1`, `instContMDiffVectorBundleOfSomeENatTopOfLEInfty`, `instContMDiffVectorBundleOfTopWithTopENat`	61
Total	67

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` `Bundle.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`

Bundle.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` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.proj` `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` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `toFun'` `Bundle.TotalSpace.proj`	—	`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` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.proj` `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` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `toFun'` `Bundle.TotalSpace.proj`	—	`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` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.proj` `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` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `toFun'` `Bundle.TotalSpace.proj`	—	`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`	`ContMDiffWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `toFun'` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`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` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.proj` `chartedSpaceSelf` `toFun'`	—	`contMDiffAt_iff`

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` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`ContMDiff` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Bundle.Trivialization.coordChange` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`ContMDiffAt.coordChange`
`coordChangeL` 📖	mathematical	`ContMDiff` `Set` `Set.instMembership` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`ContMDiff` `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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Bundle.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` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`ContMDiffAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Bundle.Trivialization.coordChange` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`ContMDiffWithinAt.coordChange`
`coordChangeL` 📖	mathematical	`ContMDiffAt` `Set` `Set.instMembership` `Bundle.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` `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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Bundle.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` `Bundle.Trivialization.open_baseSet` `contMDiffOn_coordChangeL` `contMDiffOn_symm_coordChangeL` `Bundle.Trivialization.symm_trans_source_eq` `Bundle.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` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`ContMDiffOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Bundle.Trivialization.coordChange` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`ContMDiffWithinAt.coordChange`
`coordChangeL` 📖	mathematical	`ContMDiffOn` `Set.MapsTo` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Bundle.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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Bundle.Trivialization.coordChangeL` `trivialization_linear` `Set` `Set.instInter` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	—
`of_le` 📖	mathematical	`WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `instPreorderENat`	`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` 📖	mathematical	`ContMDiffWithinAt` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Bundle.Trivialization.toFun'` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `Bundle.Trivialization.toOpenPartialHomeomorph`	`ContMDiffWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Bundle.Trivialization.toFun'` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`congr_of_eventuallyEq` `coordChange` `Bundle.Trivialization.mem_source` `Filter.mp_mem` `continuousWithinAt` `IsOpen.mem_nhds` `Bundle.Trivialization.open_baseSet` `Filter.univ_mem'` `Bundle.Trivialization.coordChange_apply_snd`
`coordChange` 📖	mathematical	`ContMDiffWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Set` `Set.instMembership` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`ContMDiffWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Bundle.Trivialization.coordChange` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`congr_of_eventuallyEq` `RingHomInvPair.ids` `trivialization_linear` `clm_apply` `coordChangeL` `IsOpen.mem_nhds` `IsOpen.inter` `Bundle.Trivialization.open_baseSet` `Filter.mp_mem` `continuousWithinAt` `Filter.univ_mem'` `Bundle.Trivialization.coordChangeL_apply'`
`coordChangeL` 📖	mathematical	`ContMDiffWithinAt` `Set` `Set.instMembership` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`ContMDiffWithinAt` `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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Bundle.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	230 math math: `TangentBundle.tangentMap_tangentBundle_pure`, `Bundle.ContMDiffRiemannianMetric.contMDiff`, `Bundle.mdifferentiableAt_proj`, `mdifferentiableAt_sub_section`, `MDifferentiableOn.finsum_section_of_locallyFinite`, `Bundle.contMDiffOn_zeroSection`, `MDifferentiableAt.clm_bundle_apply`, `mdifferentiableWithinAt_totalSpace`, `contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt`, `ContMDiffOn.mlieBracketWithin_vectorField`, `ContMDiffWithinAt.mlieBracketWithin_vectorField`, `mdifferentiableAt_iff_localFrame_coeff`, `Bundle.Trivialization.contMDiffOn_section_baseSet_iff`, `MDifferentiableOn.smul_const_section`, `tangentMap_chart`, `ContMDiffWithinAt.sub_section`, `contMDiff_addInvariantVectorField`, `mdifferentiableWithinAt_smul_const_section`, `TangentBundle.coe_chartAt_fst`, `mdifferentiableAt_add_section`, `ContMDiffAt.finsum_section_of_locallyFinite`, `Bundle.contMDiffWithinAt_zeroSection`, `contMDiff_mulInvariantVectorField`, `Bundle.Trivialization.contMDiffOn`, `MDifferentiableWithinAt.finsum_section_of_locallyFinite`, `IsLocalFrameOn.contMDiffAt_of_coeff`, `contMDiff_equivTangentBundleProd_symm`, `mdifferentiableWithinAt_section`, `contMDiffOn_baseSet_iff_localFrame_coeff`, `ContMDiffWithinAt.add_section`, `ContMDiffAt.add_section`, `MDifferentiable.clm_bundle_apply₂`, `tangentBundle_model_space_coe_chartAt`, `Bundle.contMDiffAt_zeroSection`, `contMDiffAt_mulInvariantVectorField`, `MDifferentiable.clm_bundle_apply`, `MDifferentiableWithinAt.clm_bundle_apply₂`, `mdifferentiableAt_addInvariantVectorField`, `ContMDiff.sum_section_of_locallyFinite`, `ContMDiff.contMDiff_tangentMap`, `MDifferentiableAt.mpullback_vectorField`, `ContMDiffWithinAt.sum_section`, `MDifferentiableAt.sum_section`, `Bundle.Trivialization.mdifferentiableAt_section_iff`, `mdifferentiableAt_totalSpace`, `mdifferentiable_mulInvariantVectorField`, `chartedSpace_chartAt`, `ContMDiffOn.finsum_section_of_locallyFinite`, `MDifferentiableOn.sum_section_of_locallyFinite`, `ContMDiffWithinAt.neg_section`, `ContMDiffWithinAt.mpullbackWithin_vectorField_inter`, `mdifferentiableAt_hom_bundle`, `IsLocalFrameOn.mdifferentiableAt_of_coeff_aux`, `mdifferentiableWithinAt_neg_section`, `Bundle.TotalSpace.isManifold`, `ContMDiffAt.const_smul_section`, `contMDiff_vectorSpace_iff_contDiff`, `ContMDiffOn.mpullbackWithin_vectorField_inter`, `ContMDiffAt.clm_apply_of_inCoordinates`, `Bundle.Trivialization.mdifferentiableWithinAt_totalSpace_iff`, `MDifferentiable.mpullback_vectorField`, `mdifferentiable_smul_const_section`, `Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff`, `UniqueMDiffWithinAt.bundle_preimage'`, `exists_contMDiffOn_extend`, `MDifferentiableAt.finsum_section_of_locallyFinite`, `IsContMDiffRiemannianBundle.exists_contMDiff`, `ContMDiffAt.clm_bundle_apply`, `mdifferentiableAt_neg_section`, `Bundle.Trivialization.contMDiffOn_localFrame_baseSet`, `MDifferentiableAt.clm_bundle_apply₂`, `ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin_of_eq`, `writtenInExtChartAt_trivializationAt`, `IsLocalFrameOn.mdifferentiableOn_of_coeff`, `ContMDiffWithinAt.mpullback_vectorField_preimage`, `MDifferentiableWithinAt.mpullbackWithin_vectorField_inter_of_eq`, `MDifferentiableAt.smul_section`, `ContMDiffWithinAt.mpullback_vectorField_preimage_of_eq`, `mdifferentiableAt_extend`, `MDifferentiableWithinAt.clm_apply_of_inCoordinates`, `Bundle.mdifferentiableWithinAt_proj`, `IsLocalFrameOn.contMDiffOn`, `MDifferentiableOn.clm_bundle_apply`, `Bundle.Trivialization.mdifferentiableOn_section_iff`, `ContMDiffWithinAt.finsum_section_of_locallyFinite`, `Bundle.contMDiffWithinAt_totalSpace`, `Bundle.Trivialization.contMDiffWithinAt_iff`, `mdifferentiableWithinAt_sub_section`, `Bundle.mdifferentiableOn_proj`, `mdifferentiableWithinAt_add_section`, `ContMDiffWithinAt.mpullbackWithin_vectorField'`, `tangentBundle_model_space_coe_chartAt_symm`, `MDifferentiable.sum_section`, `ContMDiffWithinAt.clm_bundle_apply₂`, `TangentBundle.chartAt`, `IsLocalFrameOn.contMDiffAt`, `contMDiffAt_hom_bundle`, `MDifferentiable.sum_section_of_locallyFinite`, `extChartAt`, `MDifferentiableWithinAt.sum_section_of_locallyFinite`, `ContMDiffAt.mlieBracket_vectorField`, `ContMDiffOn.add_section`, `ContMDiff.finsum_section_of_locallyFinite`, `Bundle.contMDiffWithinAt_proj`, `Bundle.contMDiffAt_totalSpace`, `MDifferentiableAt.clm_apply_of_inCoordinates`, `ContMDiffWithinAt.clm_bundle_apply`, `ContMDiff.clm_bundle_apply`, `UniqueMDiffOn.tangentBundle_proj_preimage`, `tangentBundle_model_space_chartAt`, `TangentBundle.mem_chart_target_iff`, `ContMDiff.clm_bundle_apply₂`, `MDifferentiableOn.sum_section`, `contMDiffAt_extend'`, `Bundle.contMDiffOn_proj`, `Bundle.contMDiff_proj`, `MDifferentiableAt.sum_section_of_locallyFinite`, `MDifferentiableOn.mpullback_vectorField_preimage`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem_of_eq`, `tangentMap_chart_symm`, `UniqueMDiffWithinAt.bundle_preimage`, `contMDiffAt_vectorSpace_iff_contDiffAt`, `ContMDiff.neg_section`, `Bundle.mdifferentiableWithinAt_zeroSection`, `mdifferentiable_addInvariantVectorField`, `VectorField.contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `Bundle.Trivialization.contMDiff_iff`, `ContMDiffWithinAt.sum_section_of_locallyFinite`, `Bundle.contMDiff_zeroSection`, `ContDiff.mlieBracket_vectorField`, `extChartAt_target`, `contMDiffAt_localFrame_of_mem`, `mdifferentiableAt_section`, `Bundle.Trivialization.contMDiffAt_section_iff`, `Bundle.mdifferentiable_proj`, `ContMDiffWithinAt.clm_apply_of_inCoordinates`, `writtenInExtChartAt_trivializationAt_symm`, `ContMDiffAt.sub_section`, `MDifferentiableWithinAt.mpullback_vectorField_preimage`, `MDifferentiableWithinAt.clm_bundle_apply`, `ContMDiffSection.contMDiff`, `contMDiff_equivTangentBundleProd`, `UniqueMDiffOn.bundle_preimage`, `Bundle.Trivialization.contMDiffAt_iff`, `ContMDiffOn.const_smul_section`, `Bundle.contMDiffAt_section`, `Bundle.Trivialization.contMDiffWithinAt_section`, `MDifferentiableOn.mpullbackWithin_vectorField_inter`, `ContMDiffAt.clm_bundle_apply₂`, `ContMDiffWithinAt.mpullbackWithin_vectorField_inter_of_eq`, `mDifferentiableOn_sub_section`, `Bundle.Trivialization.contMDiffOn_symm`, `mdifferentiableAt_mulInvariantVectorField`, `contMDiffAt_iff_localFrame_coeff`, `ContMDiffOn.sum_section_of_locallyFinite`, `ContMDiffCovariantDerivativeOn.contMDiff`, `MDifferentiableWithinAt.mpullbackWithin_vectorField_inter`, `ContMDiffOn.contMDiffOn_tangentMapWithin`, `mdifferentiable_sub_section`, `ContMDiffWithinAt.const_smul_section`, `mdifferentiable_neg_section`, `ContMDiffAt.sum_section_of_locallyFinite`, `MDifferentiable.finsum_section_of_locallyFinite`, `ContMDiffOn.mpullback_vectorField_preimage`, `IsLocalFrameOn.contMDiffOn_of_coeff`, `exists_mdifferentiableOn_extend`, `ContMDiff.sub_section`, `MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq`, `ContMDiffWithinAt.mpullbackWithin_vectorField`, `Bundle.contMDiffAt_proj`, `contMDiffAt_addInvariantVectorField`, `contMDiff_tangentBundleModelSpaceHomeomorph`, `MDifferentiableAt.smul_const_section`, `ContMDiffAt.mpullback_vectorField_preimage`, `ContMDiffOn.smul_section_of_tsupport`, `ContMDiffWithinAt.smul_section`, `mdifferentiable_add_section`, `hom_chart`, `MDifferentiableOn.smul_section`, `TangentBundle.coe_chartAt_symm_fst`, `Bundle.contMDiffWithinAt_section`, `Bundle.mdifferentiableOn_zeroSection`, `ContMDiffSection.mdifferentiable'`, `contMDiff_tangentBundleModelSpaceHomeomorph_symm`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq`, `ContMDiffOn.sub_section`, `ContMDiffSection.mdifferentiableAt`, `MDifferentiableOn.smul_section_of_tsupport`, `ContMDiff.add_section`, `ContMDiffOn.sum_section`, `ContMDiffOn.neg_section`, `ContMDiffSection.mdifferentiable`, `Bundle.Trivialization.contMDiffOn_iff`, `mdifferentiable_smul_section`, `Bundle.mdifferentiable_zeroSection`, `Bundle.Trivialization.mdifferentiableWithinAt_section_iff`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_mem`, `VectorField.eventually_contMDiffWithinAt_mpullbackWithin_extChartAt_symm`, `IsLocalFrameOn.mdifferentiableAt_of_coeff`, `TangentBundle.chartAt_toPartialEquiv`, `ContMDiffAt.sum_section`, `ContMDiff.const_smul_section`, `contMDiffOn_vectorSpace_iff_contDiffOn`, `ContMDiffOn.clm_bundle_apply`, `Bundle.Trivialization.contMDiffOn_section_iff`, `mdifferentiableOn_add_section`, `chartedSpace_chartAt_symm_fst`, `ContMDiffSection.contMDiff_toFun`, `ContMDiffAt.smul_section`, `ContMDiffAt.neg_section`, `mdifferentiableWithinAt_hom_bundle`, `IsLocalFrameOn.contMDiffAt_of_coeff_aux`, `Bundle.mdifferentiableAt_zeroSection`, `ContMDiff.sum_section`, `mdifferentiableOn_neg_section`, `Bundle.Trivialization.mdifferentiableAt_totalSpace_iff`, `contMDiff_snd_tangentBundle_modelSpace`, `ContMDiffWithinAt.mpullbackWithin_vectorField_of_eq'`, `contMDiffWithinAt_hom_bundle`, `MDifferentiableOn.clm_bundle_apply₂`, `ContMDiffOn.clm_bundle_apply₂`, `ContMDiff.mpullback_vectorField`, `Bundle.Trivialization.Bundle.Trivialization.mdifferentiable`, `TangentBundle.mem_chart_source_iff`, `MDifferentiableWithinAt.sum_section`, `ContMDiff.smul_section`, `ContMDiffWithinAt.mpullback_vectorField_of_mem_nhdsWithin`, `MDifferentiableWithinAt.smul_section`, `ContMDiffOn.smul_section`, `contMDiffOn_iff_localFrame_coeff`
`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'` `Bundle.Trivialization.toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `trivializationAt`	—	—
`chartedSpace_chartAt` 📖	mathematical	—	`chartAt` `ModelProd` `instTopologicalSpaceModelProd` `Bundle.TotalSpace` `chartedSpace` `OpenPartialHomeomorph.trans` `instTopologicalSpaceProd` `Bundle.Trivialization.toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `trivializationAt` `OpenPartialHomeomorph.prod` `OpenPartialHomeomorph.refl`	—	`Bundle.Trivialization.coe_coe` `Bundle.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'` `ModelProd` `Bundle.TotalSpace` `instTopologicalSpaceModelProd` `OpenPartialHomeomorph.symm` `chartAt` `chartedSpace`	—	`chartedSpace_chartAt` `Bundle.Trivialization.proj_symm_apply` `OpenPartialHomeomorph.open_target` `PartialEquiv.prod_symm`
`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` `Bundle.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` `Bundle.Trivialization.baseSet` `trivializationAt` `Set.univ`	—	`extChartAt` `PartialEquiv.trans_target` `Bundle.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` `Bundle.TotalSpace` `ModelProd` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `instTopologicalSpaceProd` `chartedSpace` `prodChartedSpace` `chartedSpaceSelf` `Bundle.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` `ModelProd` `Bundle.TotalSpace` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `instTopologicalSpaceProd` `ModelWithCorners.prod` `modelWithCornersSelf` `prodChartedSpace` `chartedSpaceSelf` `chartedSpace` `Bundle.Trivialization.toFun'` `Bundle.TotalSpace.proj` `trivializationAt` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `Bundle.Trivialization.toOpenPartialHomeomorph`	—	`writtenInExtChartAt_chartAt_symm_comp`

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` `NormedAddCommGroup.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` `NormedAddCommGroup.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	`Bundle.Pretrivialization` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj` `Set` `Set.instMembership` `pretrivializationAtlas` `Set.instInter` `Bundle.Pretrivialization.baseSet`	`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` `contMDiffCoordChange` `Bundle.Pretrivialization.toFun'` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `Bundle.Pretrivialization.symm` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsContMDiff.exists_contMDiffCoordChange`
`contMDiffOn_contMDiffCoordChange` 📖	mathematical	`Bundle.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` `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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `contMDiffCoordChange` `Set` `Set.instInter` `Bundle.Pretrivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`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` `Bundle.Trivialization.coordChangeL_apply`
`mk_contMDiffCoordChange` 📖	mathematical	`Bundle.Pretrivialization` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj` `Set` `Set.instMembership` `pretrivializationAtlas` `Set.instInter` `Bundle.Pretrivialization.baseSet`	`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` `contMDiffCoordChange` `Bundle.Pretrivialization.toFun'` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `Bundle.Pretrivialization.symm` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`Bundle.Pretrivialization.mk_symm` `Bundle.Pretrivialization.coe_fst'` `Bundle.Pretrivialization.proj_symm_apply'` `contMDiffCoordChange_apply`

VectorPrebundle.IsContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_contMDiffCoordChange` 📖	mathematical	`Bundle.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` `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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `Set` `Set.instInter` `Bundle.Pretrivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `DFunLike.coe` `ContinuousLinearMap.funLike` `Bundle.Pretrivialization.toFun'` `Bundle.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` `Bundle.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` `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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Bundle.Trivialization.coordChangeL` `trivialization_linear`	—	`ContMDiffOn.contMDiffAt` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `trivialization_linear` `contMDiffOn_coordChangeL` `IsOpen.mem_nhds` `IsOpen.inter` `Bundle.Trivialization.open_baseSet`
`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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Bundle.Trivialization.coordChangeL` `trivialization_linear` `Set` `Set.instInter` `Bundle.Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`ContMDiffVectorBundle.contMDiffOn_coordChangeL`
`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` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `ContinuousLinearEquiv.symm` `Bundle.Trivialization.coordChangeL` `trivialization_linear` `Set` `Set.instInter` `Bundle.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` `Bundle.Trivialization.symm_coordChangeL`
`instContMDiffVectorBundleOfNatWithTopENat` 📖	mathematical	—	`ContMDiffVectorBundle` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`Nat.instAtLeastTwoHAddOfNat` `ContMDiffVectorBundle.of_le` `one_le_two` `WithTop.zeroLEOneClass` `WithTop.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid`
`instContMDiffVectorBundleOfNatWithTopENat_1` 📖	mathematical	—	`ContMDiffVectorBundle` `WithTop` `ENat` `WithTop.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`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