Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `ofRiemannianMetric`, `ofRiemannianMetric`, `IsRiemannianManifold`, `ofRiemannianMetric`, `ofRiemannianMetric`, `instRiemannianBundleTangentSpaceRealModelWithCornersSelf`, `normedAddCommGroupTangentSpaceVectorSpace`, `normedSpaceTangentSpaceVectorSpace`, `riemannianMetricVectorSpace`	9
Theorems `out`, `enorm_tangentSpace_vectorSpace`, `eventually_enorm_mfderivWithin_symm_extChartAt_lt`, `eventually_enorm_mfderiv_extChartAt_lt`, `eventually_norm_mfderivWithin_symm_extChartAt_comp_lt`, `eventually_norm_mfderivWithin_symm_extChartAt_lt`, `eventually_norm_mfderiv_extChartAt_lt`, `eventually_riemannianEDist_le_edist_extChartAt`, `eventually_riemannianEDist_lt`, `eventually_riemmanianEDist_lt`, `instIsRiemannianManifold`, `instIsRiemannianManifoldModelWithCornersSelfReal`, `lintegral_fderiv_lineMap_eq_edist`, `nnnorm_tangentSpace_vectorSpace`, `norm_tangentSpace_vectorSpace`, `setOf_riemannianEDist_lt_subset_nhds`, `setOf_riemannianEDist_lt_subset_nhds'`, `setOf_riemmanianEDist_lt_subset_nhds`, `setOf_riemmanianEDist_lt_subset_nhds'`	19
Total	28

EMetricSpace

Definitions

Name	Category	Theorems
`ofRiemannianMetric` 📖	CompOp	—

EmetricSpace

Definitions

Name	Category	Theorems
`ofRiemannianMetric` 📖	CompOp	—

IsRiemannianManifold

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`out` 📖	mathematical	—	`EDist.edist` `PseudoEMetricSpace.toEDist` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace`	—	—

PseudoEMetricSpace

Definitions

Name	Category	Theorems
`ofRiemannianMetric` 📖	CompOp	1 math math: `instIsRiemannianManifold`

PseudoEmetricSpace

Definitions

Name	Category	Theorems
`ofRiemannianMetric` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`IsRiemannianManifold` 📖	CompData	2 math math: `instIsRiemannianManifold`, `instIsRiemannianManifoldModelWithCornersSelfReal`
`instRiemannianBundleTangentSpaceRealModelWithCornersSelf` 📖	CompOp	4 math math: `instIsRiemannianManifoldModelWithCornersSelfReal`, `enorm_tangentSpace_vectorSpace`, `norm_tangentSpace_vectorSpace`, `nnnorm_tangentSpace_vectorSpace`
`normedAddCommGroupTangentSpaceVectorSpace` 📖	CompOp	5 math math: `eventually_enorm_mfderivWithin_symm_extChartAt_lt`, `eventually_norm_mfderivWithin_symm_extChartAt_lt`, `eventually_enorm_mfderiv_extChartAt_lt`, `eventually_norm_mfderivWithin_symm_extChartAt_comp_lt`, `eventually_norm_mfderiv_extChartAt_lt`
`normedSpaceTangentSpaceVectorSpace` 📖	CompOp	5 math math: `eventually_enorm_mfderivWithin_symm_extChartAt_lt`, `eventually_norm_mfderivWithin_symm_extChartAt_lt`, `eventually_enorm_mfderiv_extChartAt_lt`, `eventually_norm_mfderivWithin_symm_extChartAt_comp_lt`, `eventually_norm_mfderiv_extChartAt_lt`
`riemannianMetricVectorSpace` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`enorm_tangentSpace_vectorSpace` 📖	mathematical	—	`ENorm.enorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `chartedSpaceSelf` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instTopologicalSpaceTangentSpace` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `instRiemannianBundleTangentSpaceRealModelWithCornersSelf` `SeminormedAddGroup.toContinuousENorm`	—	`nnnorm_tangentSpace_vectorSpace`
`eventually_enorm_mfderivWithin_symm_extChartAt_lt` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Filter.Eventually` `ENNReal` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `instModuleTangentSpace` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `normedAddCommGroupTangentSpaceVectorSpace` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `normedSpaceTangentSpaceVectorSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Bundle.instInnerProductSpaceReal` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'` `ENNReal.ofNNReal` `nhdsWithin`	—	`TangentSpace.vectorBundle` `RingHomIsometric.ids` `eventually_norm_mfderivWithin_symm_extChartAt_lt` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `Filter.mp_mem` `Filter.univ_mem'` `norm_nonneg`
`eventually_enorm_mfderiv_extChartAt_lt` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Filter.Eventually` `ENNReal` `ENNReal.instPartialOrder` `ENorm.enorm` `ContinuousLinearMap` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `instModuleTangentSpace` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `normedAddCommGroupTangentSpaceVectorSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Bundle.instInnerProductSpaceReal` `normedSpaceTangentSpaceVectorSpace` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `mfderiv` `ENNReal.ofNNReal` `nhds`	—	`TangentSpace.vectorBundle` `RingHomIsometric.ids` `eventually_norm_mfderiv_extChartAt_lt` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `Filter.mp_mem` `Filter.univ_mem'` `norm_nonneg`
`eventually_norm_mfderivWithin_symm_extChartAt_comp_lt` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Filter.Eventually` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `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` `PartialEquiv.symm` `instModuleTangentSpace` `ContinuousLinearMap.hasOpNorm` `normedAddCommGroupTangentSpaceVectorSpace` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `normedSpaceTangentSpaceVectorSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Bundle.instInnerProductSpaceReal` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'` `nhds`	—	`TangentSpace.vectorBundle` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `eventually_norm_symmL_trivializationAt_lt` `chart_source_mem_nhds` `Filter.mp_mem` `Filter.univ_mem'` `PartialEquiv.left_inv` `ModelWithCorners.source_eq` `Set.inter_univ` `TangentBundle.symmL_trivializationAt`
`eventually_norm_mfderivWithin_symm_extChartAt_lt` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Filter.Eventually` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `PartialEquiv.toFun` `PartialEquiv.symm` `extChartAt` `instModuleTangentSpace` `ContinuousLinearMap.hasOpNorm` `normedAddCommGroupTangentSpaceVectorSpace` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `normedSpaceTangentSpaceVectorSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Bundle.instInnerProductSpaceReal` `mfderivWithin` `Set.range` `ModelWithCorners.toFun'` `nhdsWithin`	—	`TangentSpace.vectorBundle` `eventually_norm_mfderivWithin_symm_extChartAt_comp_lt` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `continuousAt_extChartAt_symm` `Filter.mp_mem` `extChartAt_target_mem_nhdsWithin` `nhdsWithin_le_nhds` `ContinuousAt.preimage_mem_nhds` `Filter.univ_mem'` `PartialEquiv.right_inv`
`eventually_norm_mfderiv_extChartAt_lt` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Filter.Eventually` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `TangentSpace` `instTopologicalSpaceTangentSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `PartialEquiv.toFun` `extChartAt` `instModuleTangentSpace` `ContinuousLinearMap.hasOpNorm` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `normedAddCommGroupTangentSpaceVectorSpace` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `Bundle.instInnerProductSpaceReal` `normedSpaceTangentSpaceVectorSpace` `mfderiv` `nhds`	—	`TangentSpace.vectorBundle` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `eventually_norm_trivializationAt_lt` `chart_source_mem_nhds` `Filter.mp_mem` `Filter.univ_mem'` `TangentBundle.continuousLinearMapAt_trivializationAt`
`eventually_riemannianEDist_le_edist_extChartAt` 📖	mathematical	—	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Filter.Eventually` `ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `EDist.edist` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `PartialEquiv.toFun` `extChartAt` `nhds`	—	`TangentSpace.vectorBundle` `RingHomIsometric.ids` `eventually_enorm_mfderivWithin_symm_extChartAt_lt` `Metric.mem_nhdsWithin_iff` `Filter.inter_mem` `extChartAt_target_mem_nhdsWithin` `extChartAt_preimage_mem_nhds_of_mem_nhdsWithin` `ModelWithCorners.source_eq` `Set.inter_univ` `Set.inter_comm` `inter_mem_nhdsWithin` `Metric.ball_mem_nhds` `Filter.mp_mem` `chart_source_mem_nhds` `Filter.univ_mem'` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor_1` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Set.Subset.trans` `Convex.segment_subset` `Convex.inter` `convex_ball` `ModelWithCorners.convex_range` `dist_self` `ContMDiff.contMDiffOn` `contMDiff_iff_contDiff` `ContinuousAffineMap.contDiff` `Manifold.riemannianEDist_le_pathELength` `instENormSMulClass` `NormedSpace.toNormSMulClass` `ContMDiffOn.comp` `contMDiffOn_extChartAt_symm` `AffineMap.lineMap_apply_zero` `ModelWithCorners.left_inv` `OpenPartialHomeomorph.left_inv` `AffineMap.lineMap_apply_one` `zero_le_one` `Real.instZeroLEOneClass` `LE.le.trans` `lintegral_fderiv_lineMap_eq_edist` `Manifold.pathELength_eq_lintegral_mfderivWithin_Icc` `MeasureTheory.lintegral_const_mul'` `ENNReal.coe_ne_top` `MeasureTheory.setLIntegral_mono'` `measurableSet_Icc` `BorelSpace.opensMeasurable` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `RingHomCompTriple.ids` `mfderivWithin_comp` `mdifferentiableWithinAt_extChartAt_symm` `ContMDiffOn.mdifferentiableOn` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.preimage_mono` `extChartAt_target_subset_range` `uniqueMDiffWithinAt_iff_uniqueDiffWithinAt` `uniqueDiffOn_Icc` `zero_lt_one` `RCLike.charZero_rclike` `ContinuousLinearMap.le_opNorm_enorm` `mul_le_mul'` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `covariant_swap_mul_of_covariant_mul` `LT.lt.le` `mfderivWithin_eq_fderivWithin` `le_of_eq`
`eventually_riemannianEDist_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal`	`Filter.Eventually` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `nhds`	—	`TangentSpace.vectorBundle` `eventually_riemannianEDist_le_edist_extChartAt` `ContinuousAt.preimage_mem_nhds` `continuousAt_extChartAt` `Metric.eball_mem_nhds` `ENNReal.div_pos` `LT.lt.ne'` `Filter.mp_mem` `Filter.univ_mem'` `LE.le.trans_lt` `mul_comm` `ENNReal.lt_div_iff_mul_lt` `Nat.cast_zero`
`eventually_riemmanianEDist_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal`	`Filter.Eventually` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `nhds`	—	`eventually_riemannianEDist_lt`
`instIsRiemannianManifold` 📖	mathematical	—	`IsRiemannianManifold` `PseudoEMetricSpace.ofRiemannianMetric`	—	`TangentSpace.vectorBundle`
`instIsRiemannianManifoldModelWithCornersSelfReal` 📖	mathematical	—	`IsRiemannianManifold` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `chartedSpaceSelf` `instRiemannianBundleTangentSpaceRealModelWithCornersSelf`	—	`le_antisymm` `fact_one_le_two_ennreal` `Manifold.riemannianEDist_def` `zero_le_one` `Real.instZeroLEOneClass` `contMDiffOn_iff_contDiffOn` `ContMDiff.comp_contMDiffOn` `contMDiffOn_projIcc` `LT.lt.le` `Fact.out` `Manifold.lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc` `Manifold.pathELength_eq_lintegral_mfderivWithin_Icc` `mfderivWithin_eq_fderivWithin` `enorm_tangentSpace_vectorSpace` `PseudoEMetricSpace.edist_comm` `edist_eq_enorm_sub` `Real.instIsOrderedRing` `Set.projIcc_left` `Path.source` `Set.projIcc_right` `Path.target` `LE.le.trans_eq` `enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor_1` `Manifold.riemannianEDist_le_pathELength` `instENormSMulClass` `NormedSpace.toNormSMulClass` `ContDiff.contDiffOn` `ContinuousAffineMap.contDiff` `AffineMap.lineMap_apply_zero` `AffineMap.lineMap_apply_one` `lintegral_fderiv_lineMap_eq_edist`
`lintegral_fderiv_lineMap_eq_edist` 📖	mathematical	—	`MeasureTheory.lintegral` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne` `ENorm.enorm` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `Real.pseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `Real.instAddCommGroup` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `RCLike.toInnerProductSpaceReal` `ContinuousLinearMap.funLike` `fderivWithin` `ContinuousAffineMap` `Real.instRing` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `ContinuousAffineMap.instFunLike` `ContinuousAffineMap.lineMap` `IsBoundedSMul.continuousSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddTorsor.toContinuousVAdd` `SeminormedAddGroup.toAddGroup` `instIsTopologicalAddTorsor_1` `EDist.edist` `PseudoEMetricSpace.toEDist` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace`	—	`PseudoEMetricSpace.edist_comm` `edist_eq_enorm_sub` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `Real.volume_Icc` `sub_zero` `ENNReal.ofReal_one` `mul_one` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddTorsor.toContinuousVAdd` `instIsTopologicalAddTorsor_1` `MeasureTheory.setLIntegral_congr_fun` `measurableSet_Icc` `BorelSpace.opensMeasurable` `Real.borelSpace` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ContinuousAffineMap.fderiv` `IsScalarTower.left` `AffineMap.lineMap_linear` `one_smul` `fderivWithin_eq_fderiv` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `uniqueDiffOn_Icc` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ContinuousAffineMap.differentiableAt`
`nnnorm_tangentSpace_vectorSpace` 📖	mathematical	—	`NNNorm.nnnorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `chartedSpaceSelf` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instTopologicalSpaceTangentSpace` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `instRiemannianBundleTangentSpaceRealModelWithCornersSelf`	—	`norm_nonneg` `norm_tangentSpace_vectorSpace`
`norm_tangentSpace_vectorSpace` 📖	mathematical	—	`Norm.norm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `modelWithCornersSelf` `chartedSpaceSelf` `NormedAddCommGroup.toNorm` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instTopologicalSpaceTangentSpace` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `instRiemannianBundleTangentSpaceRealModelWithCornersSelf`	—	`norm_eq_sqrt_real_inner`
`setOf_riemannianEDist_lt_subset_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Set.instHasSubset` `setOf` `ENNReal` `ENNReal.instPartialOrder` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `ENNReal.ofNNReal`	—	`TangentSpace.vectorBundle` `RingHomIsometric.ids` `eventually_enorm_mfderiv_extChartAt_lt` `Filter.inter_mem` `extChartAt_source_mem_nhds` `exists_mem_nhds_isClosed_subset` `ModelWithCorners.source_eq` `Set.inter_univ` `Filter.HasBasis.mem_iff` `nhds_basis_opens'` `Metric.mem_nhds_iff` `extChartAt_preimage_mem_nhds` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Manifold.exists_lt_locally_constant_of_riemannianEDist_lt` `instENormSMulClass` `NormedSpace.toNormSMulClass` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `mem_of_mem_nhds` `IsClosed.inter` `IsClosed.preimage` `ContMDiff.continuous` `isClosed_Icc` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsClosed.Icc_subset_of_forall_mem_nhdsGT_of_Icc_subset` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `ContMDiffOn.comp` `contMDiffOn_extChartAt` `ContMDiff.contMDiffOn` `LE.le.eq_or_lt` `sub_self` `enorm_zero` `enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc` `contMDiffOn_iff_contDiffOn` `mfderivWithin_eq_fderivWithin` `MeasureTheory.setLIntegral_mono'` `measurableSet_Icc` `BorelSpace.opensMeasurable` `Real.borelSpace` `RingHomCompTriple.ids` `mfderiv_comp_mfderivWithin` `mdifferentiableAt_extChartAt` `MDifferentiable.mdifferentiableOn` `ContMDiff.mdifferentiable` `one_ne_zero` `WithTop.charZero` `uniqueMDiffWithinAt_iff_uniqueDiffWithinAt` `uniqueDiffOn_Icc` `LE.le.trans` `ContinuousLinearMap.le_opNorm_enorm` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `MeasureTheory.lintegral_const_mul'` `ENNReal.coe_ne_top` `Manifold.pathELength_eq_lintegral_mfderivWithin_Icc` `mul_le_mul_right` `Manifold.pathELength_mono` `le_refl` `le_of_lt` `ENNReal.mul_lt_mul_right` `ne_of_gt` `ENNReal.coe_pos` `LT.lt.trans_eq` `ENNReal.coe_div` `LT.lt.ne'` `ENNReal.eq_div_iff` `Metric.eball_coe` `Metric.mem_eball` `edist_eq_enorm_sub` `PartialEquiv.left_inv` `Set.right_mem_Icc` `Set.mem_preimage` `Continuous.continuousWithinAt` `Filter.mem_of_superset` `IsOpen.mem_nhds` `zero_le_one` `le_rfl`
`setOf_riemannianEDist_lt_subset_nhds'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Set.instHasSubset` `setOf` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace`	—	`TangentSpace.vectorBundle` `setOf_riemannianEDist_lt_subset_nhds` `Nat.cast_zero`
`setOf_riemmanianEDist_lt_subset_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Set.instHasSubset` `setOf` `ENNReal` `ENNReal.instPartialOrder` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace` `ENNReal.ofNNReal`	—	`setOf_riemannianEDist_lt_subset_nhds`
`setOf_riemmanianEDist_lt_subset_nhds'` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `Set.instHasSubset` `setOf` `Manifold.riemannianEDist` `ContinuousENorm.toENorm` `TangentSpace` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `instTopologicalSpaceTangentSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.instNormedAddCommGroupOfRiemannianBundle` `instAddCommGroupTangentSpace` `instModuleTangentSpace` `instIsTopologicalAddGroupTangentSpace` `instContinuousConstSMulTangentSpace`	—	`setOf_riemannianEDist_lt_subset_nhds'`

---

← Back to Index