Documentation Verification Report

UniqueDifferential

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

Statistics

Metric	Count
Definitions	0
Theorems `bundle_preimage`, `image_denseRange`, `image_denseRange'`, `uniqueDiffOn_inter_preimage`, `uniqueDiffOn_target_inter`, `uniqueDiffWithinAt_range_inter`, `uniqueMDiffOn_preimage`, `uniqueMDiffOn_target_inter`, `bundle_preimage`, `bundle_preimage'`, `image_denseRange`, `preimage_openPartialHomeomorph`	12
Total	12

UniqueMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bundle_preimage` 📖	mathematical	`UniqueMDiffOn`	`UniqueMDiffOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Set.preimage` `Bundle.TotalSpace.proj`	—	`UniqueMDiffWithinAt.bundle_preimage`
`image_denseRange` 📖	mathematical	`UniqueMDiffOn` `MDifferentiableOn` `DenseRange` `TangentSpace` `instTopologicalSpaceTangentSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `instModuleTangentSpace` `ContinuousLinearMap.funLike` `mfderivWithin`	`UniqueMDiffOn` `Set.image`	—	`image_denseRange'` `MDifferentiableWithinAt.hasMFDerivWithinAt`
`image_denseRange'` 📖	mathematical	`UniqueMDiffOn` `HasMFDerivWithinAt` `DenseRange` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike`	`UniqueMDiffOn` `Set.image`	—	`Set.forall_mem_image` `UniqueMDiffWithinAt.image_denseRange`
`uniqueDiffOn_inter_preimage` 📖	mathematical	`UniqueMDiffOn` `ContinuousOn`	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instInter` `PartialEquiv.target` `extChartAt` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `PartialEquiv.source`	—	`uniqueDiffOn_target_inter` `UniqueMDiffWithinAt.inter'` `ContinuousWithinAt.preimage_mem_nhdsWithin` `IsOpen.mem_nhds` `isOpen_extChartAt_source`
`uniqueDiffOn_target_inter` 📖	mathematical	`UniqueMDiffOn`	`UniqueDiffOn` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instInter` `PartialEquiv.target` `extChartAt` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm`	—	`uniqueDiffOn` `uniqueMDiffOn_target_inter`
`uniqueDiffWithinAt_range_inter` 📖	mathematical	`UniqueMDiffOn` `Set` `Set.instMembership` `Set.instInter` `PartialEquiv.target` `extChartAt` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm`	`UniqueDiffWithinAt` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Set` `Set.instInter` `Set.range` `ModelWithCorners.toFun'` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt`	—	`UniqueDiffWithinAt.mono` `uniqueDiffOn_target_inter` `Set.inter_subset_inter_left` `extChartAt_target_subset_range`
`uniqueMDiffOn_preimage` 📖	mathematical	`UniqueMDiffOn` `OpenPartialHomeomorph.MDifferentiable`	`UniqueMDiffOn` `Set` `Set.instInter` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv` `Set.preimage` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm`	—	`UniqueMDiffWithinAt.preimage_openPartialHomeomorph` `OpenPartialHomeomorph.map_target` `OpenPartialHomeomorph.right_inv`
`uniqueMDiffOn_target_inter` 📖	mathematical	`UniqueMDiffOn`	`UniqueMDiffOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Set` `Set.instInter` `PartialEquiv.target` `extChartAt` `Set.preimage` `PartialEquiv.toFun` `PartialEquiv.symm`	—	`PartialEquiv.image_source_inter_eq'` `Set.inter_comm` `extChartAt_source` `image_denseRange'` `inter` `OpenPartialHomeomorph.open_source` `hasMFDerivWithinAt_extChartAt` `Function.Surjective.denseRange` `OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective` `mdifferentiable_chart`

UniqueMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bundle_preimage` 📖	mathematical	`UniqueMDiffWithinAt` `Bundle.TotalSpace.proj`	`UniqueMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Set.preimage` `Bundle.TotalSpace.proj`	—	`inter` `IsOpen.mem_nhds` `Bundle.Trivialization.open_baseSet` `FiberBundle.mem_baseSet_trivializationAt'` `Set.inter_subset_right` `mono`
`bundle_preimage'` 📖	mathematical	`UniqueMDiffWithinAt`	`UniqueMDiffWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Set.preimage` `Bundle.TotalSpace.proj`	—	`bundle_preimage`
`image_denseRange` 📖	mathematical	`UniqueMDiffWithinAt` `HasMFDerivWithinAt` `DenseRange` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike`	`UniqueMDiffWithinAt` `Set.image`	—	`inter'` `extChartAt_source_mem_nhds` `UniqueDiffWithinAt.congr_pt` `UniqueDiffWithinAt.mono` `HasFDerivWithinAt.uniqueDiffWithinAt` `HasFDerivWithinAt.mono` `ModelWithCorners.source_eq` `Set.inter_univ` `PartialEquiv.left_inv` `Set.mem_range_self` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv`
`preimage_openPartialHomeomorph` 📖	mathematical	`UniqueMDiffWithinAt` `OpenPartialHomeomorph.MDifferentiable` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv`	`UniqueMDiffWithinAt` `Set` `Set.instInter` `PartialEquiv.target` `OpenPartialHomeomorph.toPartialEquiv` `Set.preimage` `OpenPartialHomeomorph.toFun'` `OpenPartialHomeomorph.symm`	—	`OpenPartialHomeomorph.image_source_inter_eq'` `Set.inter_comm` `image_denseRange` `inter` `IsOpen.mem_nhds` `OpenPartialHomeomorph.open_source` `HasMFDerivAt.hasMFDerivWithinAt` `MDifferentiableAt.hasMFDerivAt` `OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt` `Function.Surjective.denseRange` `OpenPartialHomeomorph.MDifferentiable.mfderiv_surjective`

---

← Back to Index