Documentation Verification Report

ContMDiffMFDeriv

📁 Source: Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Statistics

Metric	Count
Definitions `equivTangentBundleProd`	1
Theorems `contMDiff_tangentMap`, `continuous_tangentMap`, `mfderiv`, `mfderiv_apply`, `mfderiv_const`, `mdifferentiable`, `mdifferentiable'`, `mdifferentiableAt`, `contMDiffOn_tangentMapWithin`, `continuousOn_tangentMapWithin`, `mfderivWithin`, `mfderivWithin_apply`, `mfderivWithin_const`, `tangentMap_tangentBundle_pure`, `contMDiff_equivTangentBundleProd`, `contMDiff_equivTangentBundleProd_symm`, `equivTangentBundleProd_apply`, `equivTangentBundleProd_eq_tangentMap_prod_tangentMap`, `equivTangentBundleProd_symm_apply_proj`, `equivTangentBundleProd_symm_apply_snd`	20
Total	21

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiff_tangentMap` 📖	mathematical	`ContMDiff` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `TangentBundle` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `TangentSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `tangentMap`	—	`contMDiffOn_univ` `tangentMapWithin_univ` `ContMDiffOn.contMDiffOn_tangentMapWithin` `uniqueMDiffOn_univ`
`continuous_tangentMap` 📖	mathematical	`ContMDiff` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`Continuous` `TangentBundle` `instTopologicalSpaceTangentBundle` `tangentMap`	—	`continuousOn_univ` `tangentMapWithin_univ` `ContMDiffOn.continuousOn_tangentMapWithin` `contMDiffOn_univ` `uniqueMDiffOn_univ`

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mfderiv` 📖	mathematical	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `modelWithCornersSelf` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `inTangentCoordinates` `mfderiv`	—	`RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `contMDiffWithinAt_univ` `ContMDiffWithinAt.mfderivWithin` `Set.univ_prod_univ` `Set.mem_univ` `Set.mapsTo_univ` `uniqueMDiffOn_univ`
`mfderiv_apply` 📖	mathematical	`ContMDiffAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `chartedSpaceSelf` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `inTangentCoordinates` `mfderiv`	—	`clm_apply` `comp_of_eq` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `mfderiv`
`mfderiv_const` 📖	mathematical	`ContMDiffAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `modelWithCornersSelf` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `inTangentCoordinates` `mfderiv`	—	`mfderiv` `comp` `contMDiffAt_snd` `contMDiffAt_id`

ContMDiffMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiable` 📖	mathematical	—	`MDifferentiable` `DFunLike.coe` `ContMDiffMap` `WithTop.some` `ENat` `Top.top` `instTopENat` `instFunLike`	—	`mdifferentiable'`
`mdifferentiable'` 📖	mathematical	—	`MDifferentiable` `DFunLike.coe` `ContMDiffMap` `instFunLike`	—	`ContMDiff.mdifferentiable` `contMDiff`
`mdifferentiableAt` 📖	mathematical	—	`MDifferentiableAt` `DFunLike.coe` `ContMDiffMap` `WithTop.some` `ENat` `Top.top` `instTopENat` `instFunLike`	—	`mdifferentiable`

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffOn_tangentMapWithin` 📖	mathematical	`ContMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `UniqueMDiffOn`	`Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `TangentBundle` `instTopologicalSpaceTangentBundle` `FiberBundle.chartedSpace` `TangentSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `tangentMapWithin` `Set.preimage` `Bundle.TotalSpace.proj`	—	`contMDiffWithinAt_id` `ContMDiffWithinAt.comp` `ContMDiffWithinAt.of_le` `LE.le.trans` `le_self_add` `WithTop.canonicallyOrderedAdd` `Bundle.contMDiffWithinAt_proj` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TangentSpace.vectorBundle` `ContMDiffWithinAt.mfderivWithin_const` `ContMDiffWithinAt.clm_apply_of_inCoordinates`
`continuousOn_tangentMapWithin` 📖	mathematical	`ContMDiffOn` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `UniqueMDiffOn`	`ContinuousOn` `TangentBundle` `instTopologicalSpaceTangentBundle` `tangentMapWithin` `Set.preimage` `Bundle.TotalSpace.proj` `TangentSpace`	—	`contMDiffOn_tangentMapWithin` `continuousOn`

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mfderivWithin` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd` `Set.instMembership` `Set.MapsTo` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `UniqueMDiffOn`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `modelWithCornersSelf` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `inTangentCoordinates` `mfderivWithin`	—	`Set.inter_subset_left` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousWithinAt.comp` `continuousWithinAt` `ContinuousWithinAt.prodMk` `continuousWithinAt_id` `ContinuousWithinAt.preimage_mem_nhdsWithin` `extChartAt_source_mem_nhds` `contMDiffWithinAt_iff_contMDiffWithinAt_nhdsWithin` `IsManifold.prod` `of_le` `LE.le.trans` `self_le_add_left` `WithTop.canonicallyOrderedAdd` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.Tendsto.eventually` `ContinuousWithinAt.tendsto_nhdsWithin` `Set.insert_eq_of_mem` `Filter.univ_mem'` `comp` `prodMk` `contMDiffWithinAt_const` `contMDiffWithinAt_id` `mono` `Set.prod_mono_left` `ContDiffWithinAt.fderivWithin` `Set.inter_subset_inter_right` `Set.prod_mono_right` `extChartAt_target_subset_range` `Set.ext` `ModelWithCorners.target_eq` `contMDiffWithinAt_iff` `ModelWithCorners.range_prod` `extChartAt_prod` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `ContDiffWithinAt.mono` `UniqueMDiffOn.uniqueDiffOn_target_inter` `Nat.cast_one` `ModelWithCorners.source_eq` `Set.inter_univ` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_subset_iff` `PartialEquiv.map_source` `Set.inter_subset_right` `Set.mem_preimage` `PartialEquiv.left_inv` `contMDiffWithinAt_iff_source` `congr_of_eventuallyEq_of_mem` `nhdsWithin_mono` `UniqueDiffWithinAt.uniqueMDiffWithinAt` `MDifferentiableWithinAt.mfderivWithin_mono` `mdifferentiableWithinAt_extChartAt_symm` `RingHomCompTriple.ids` `inTangentCoordinates_eq_mfderiv_comp` `mfderivWithin_comp_of_eq` `mdifferentiableWithinAt` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `MDifferentiableWithinAt.mono` `mfderiv_comp_mfderivWithin_of_eq` `mdifferentiableAt_extChartAt` `MDifferentiableWithinAt.comp` `mfderivWithin_eq_fderivWithin` `mono_of_mem_nhdsWithin` `Filter.inter_mem`
`mfderivWithin_apply` 📖	mathematical	`ContMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `SProd.sprod` `Set` `Set.instSProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `chartedSpaceSelf` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set.MapsTo` `Set.instMembership` `UniqueMDiffOn`	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `RingHom.id` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `inTangentCoordinates` `mfderivWithin`	—	`clm_apply` `comp_of_eq` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `mfderivWithin`
`mfderivWithin_const` 📖	mathematical	`ContMDiffWithinAt` `WithTop` `ENat` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithTop.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Set` `Set.instMembership` `UniqueMDiffOn`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `modelWithCornersSelf` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `inTangentCoordinates` `mfderivWithin`	—	`comp` `contMDiffWithinAt_snd` `Set.mapsTo_snd_prod` `mfderivWithin` `contMDiffWithinAt_id` `Set.mapsTo_id`

TangentBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tangentMap_tangentBundle_pure` 📖	mathematical	—	`tangentMap` `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` `Bundle.zeroSection` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `instAddCommGroupTangentSpace` `Bundle.TotalSpace.proj` `Bundle.TotalSpace.snd` `NormedAddCommGroup.toAddCommGroup`	—	`IsOpen.mem_nhds` `IsOpen.preimage` `ModelWithCorners.continuous_invFun` `OpenPartialHomeomorph.open_target` `ModelWithCorners.left_inv` `ContMDiff.mdifferentiableAt` `Bundle.contMDiff_zeroSection` `TangentSpace.vectorBundle` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `fderivWithin_eq_fderiv` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Prod.continuousAdd` `Prod.continuousSMul` `Prod.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `ModelWithCorners.uniqueDiffWithinAt_image` `DifferentiableAt.prodMk` `differentiableAt_id` `differentiableAt_const` `DifferentiableAt.fderiv_prodMk` `differentiableAt_fun_id` `fderiv_id'` `fderiv_fun_const` `FiberBundle.chartedSpace_chartAt` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `fderivWithin_inter` `fderivWithin_congr` `OpenPartialHomeomorph.right_inv` `ModelWithCorners.right_inv` `OpenPartialHomeomorph.left_inv`

(root)

Definitions

Name	Category	Theorems
`equivTangentBundleProd` 📖	CompOp	6 math math: `contMDiff_equivTangentBundleProd_symm`, `equivTangentBundleProd_apply`, `equivTangentBundleProd_symm_apply_snd`, `contMDiff_equivTangentBundleProd`, `equivTangentBundleProd_eq_tangentMap_prod_tangentMap`, `equivTangentBundleProd_symm_apply_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiff_equivTangentBundleProd` 📖	mathematical	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.tangent` `ModelWithCorners.prod` `TangentBundle` `instTopologicalSpaceProd` `prodChartedSpace` `instTopologicalSpaceTangentBundle` `IsManifold.prod` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `FiberBundle.chartedSpace` `TangentSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivTangentBundleProd`	—	`IsManifold.prod` `equivTangentBundleProd_eq_tangentMap_prod_tangentMap` `ContMDiff.prodMk` `ContMDiff.contMDiff_tangentMap` `contMDiff_fst` `le_rfl` `contMDiff_snd`
`contMDiff_equivTangentBundleProd_symm` 📖	mathematical	—	`ContMDiff` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `ModelWithCorners.tangent` `TangentBundle` `instTopologicalSpaceProd` `instTopologicalSpaceTangentBundle` `prodChartedSpace` `FiberBundle.chartedSpace` `TangentSpace` `instTopologicalSpaceTangentSpace` `TangentSpace.fiberBundle` `IsManifold.prod` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivTangentBundleProd`	—	`IsManifold.prod` `Set.range_prodMap` `UniqueDiffWithinAt.prod` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ModelWithCorners.uniqueDiffWithinAt_image` `Bundle.contMDiffAt_totalSpace` `ContMDiffAt.prodMap` `Bundle.contMDiffAt_proj` `contMDiffAt_prod_module_iff` `contMDiffAt_fst` `ContMDiffAt.congr_of_eventuallyEq` `Filter.mp_mem` `chart_source_mem_nhds` `Filter.univ_mem'` `ContDiffWithinAt.differentiableWithinAt` `contDiffWithinAt_ext_coord_change` `ModelWithCorners.target_eq` `ModelWithCorners.source_eq` `Set.inter_univ` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `DifferentiableWithinAt.comp` `differentiableWithinAt_fst` `DifferentiableWithinAt.fderivWithin_prodMk` `differentiableWithinAt_snd` `RingHomCompTriple.ids` `fderivWithin_comp` `Set.mapsTo_fst_prod` `ContinuousLinearMap.comp.congr_simp` `fderivWithin_fst` `contMDiffAt_snd` `Set.mapsTo_snd_prod` `fderivWithin_snd`
`equivTangentBundleProd_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TangentBundle` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivTangentBundleProd` `TangentSpace` `Bundle.TotalSpace.proj` `Bundle.TotalSpace.snd`	—	—
`equivTangentBundleProd_eq_tangentMap_prod_tangentMap` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TangentBundle` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivTangentBundleProd` `tangentMap`	—	`tangentMap_prodFst` `tangentMap_prodSnd`
`equivTangentBundleProd_symm_apply_proj` 📖	mathematical	—	`Bundle.TotalSpace.proj` `TangentSpace` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `DFunLike.coe` `Equiv` `TangentBundle` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivTangentBundleProd`	—	—
`equivTangentBundleProd_symm_apply_snd` 📖	mathematical	—	`Bundle.TotalSpace.snd` `TangentSpace` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `instTopologicalSpaceProd` `prodChartedSpace` `DFunLike.coe` `Equiv` `TangentBundle` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivTangentBundleProd`	—	—

---

← Back to Index