Documentation Verification Report

Tangent

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

Statistics

Metric	Count
Definitions `tangentBundleModelSpaceDiffeomorph`	1
Theorems `tangentBundle_proj_preimage`, `inTangentCoordinates_eq_mfderiv_comp`, `mfderiv_chartAt_eq_tangentCoordChange`, `tangentMap_chart`, `tangentMap_chart_symm`	5
Total	6

UniqueMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tangentBundle_proj_preimage` 📖	mathematical	`UniqueMDiffOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `Bundle.TotalSpace` `TangentSpace` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `Set.preimage` `Bundle.TotalSpace.proj`	—	`bundle_preimage`

(root)

Definitions

Name	Category	Theorems
`tangentBundleModelSpaceDiffeomorph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inTangentCoordinates_eq_mfderiv_comp` 📖	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` `TangentSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `RingHomCompTriple.ids` `mfderiv` `mfderivWithin` `PartialEquiv.symm` `Set.range` `ModelWithCorners.toFun'`	—	`RingHomCompTriple.ids` `inTangentCoordinates_eq` `tangentBundleCore_coordChange` `mdifferentiableAt_extChartAt` `PartialEquiv.trans_refl` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId` `Set.range_id` `Set.inter_univ` `mdifferentiableWithinAt_extChartAt_symm` `PartialEquiv.map_source` `ModelWithCorners.source_eq` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `CompTriple.instComp_id`
`mfderiv_chartAt_eq_tangentCoordChange` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt`	`mfderiv` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'` `tangentCoordChange`	—	`mdifferentiableAt_atlas` `ChartedSpace.chart_mem_atlas` `PartialEquiv.refl_trans`
`tangentMap_chart` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Bundle.TotalSpace.proj` `TangentSpace`	`tangentMap` `chartedSpaceSelf` `OpenPartialHomeomorph.toFun'` `DFunLike.coe` `Equiv` `Bundle.TotalSpace` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Bundle.TotalSpace.toProd` `TangentBundle` `ModelProd` `instTopologicalSpaceTangentBundle` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle`	—	`MDifferentiableAt.mfderiv` `mdifferentiableAt_atlas` `chart_mem_atlas`
`tangentMap_chart_symm` 📖	mathematical	`Set` `Set.instMembership` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv` `chartAt` `Bundle.TotalSpace.proj` `TangentSpace` `chartedSpaceSelf`	`tangentMap` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm` `ModelProd` `TangentBundle` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `DFunLike.coe` `Equiv` `Bundle.TotalSpace` `EquivLike.toFunLike` `Equiv.instEquivLike` `Bundle.TotalSpace.toProd`	—	`MDifferentiableAt.mfderiv` `mdifferentiableAt_atlas_symm` `chart_mem_atlas` `mem_chart_source` `PartialEquiv.refl_trans` `OpenPartialHomeomorph.right_inv`

---

← Back to Index