PathELength

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

Statistics

Metric	Count
Definitions pathELength, riemannianEDist	2
Theorems exists_lt_locally_constant_of_riemannianEDist_lt, exists_lt_of_riemannianEDist_lt, lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, pathELength_add, pathELength_comp_of_antitoneOn, pathELength_comp_of_monotoneOn, pathELength_congr, pathELength_congr_Ioo, pathELength_def, pathELength_eq_lintegral_mfderivWithin_Icc, pathELength_eq_lintegral_mfderiv_Icc, pathELength_eq_lintegral_mfderiv_Ioo, pathELength_mono, pathELength_self, riemannianEDist_comm, riemannianEDist_def, riemannianEDist_le_pathELength, riemannianEDist_self, riemannianEDist_triangle	19
Total	21

Manifold

Definitions

Name	Category	Theorems
pathELength 📖	CompOp	15 math math: pathELength_eq_lintegral_mfderiv_Ioo, riemannianEDist_le_pathELength, pathELength_def, pathELength_eq_lintegral_mfderivWithin_Icc, pathELength_congr_Ioo, pathELength_comp_of_antitoneOn, pathELength_comp_of_monotoneOn, pathELength_congr, pathELength_add, pathELength_eq_lintegral_mfderiv_Icc, lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc, pathELength_self, exists_lt_of_riemannianEDist_lt, pathELength_mono, exists_lt_locally_constant_of_riemannianEDist_lt
riemannianEDist 📖	CompOp	13 math math: setOf_riemmanianEDist_lt_subset_nhds, riemannianEDist_le_pathELength, eventually_riemmanianEDist_lt, riemannianEDist_self, riemannianEDist_def, riemannianEDist_comm, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, setOf_riemmanianEDist_lt_subset_nhds', riemannianEDist_triangle, IsRiemannianManifold.out, setOf_riemannianEDist_lt_subset_nhds', eventually_riemannianEDist_lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lt_locally_constant_of_riemannianEDist_lt 📖	mathematical	ENormSMulClass Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder riemannianEDist Real.instLT	ContMDiff Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat pathELength Filter.EventuallyEq nhds	—	exists_lt_of_riemannianEDist_lt exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt inv_mul_eq_div one_le_div₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono lt_of_not_ge Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_nonpos_of_le contMDiffOn_univ ContMDiffOn.comp contMDiff_iff_contDiff ContDiff.fun_comp Real.smoothTransition.contDiff ContDiff.mul contDiff_const ContDiff.sub contDiff_fun_id Real.smoothTransition.nonneg Real.smoothTransition.le_one pathELength_comp_of_monotoneOn Monotone.monotoneOn Monotone.comp Real.smoothTransition.monotone mul_le_mul_of_nonneg_left sub_le_sub_right ContDiffOn.differentiableOn ContDiff.contDiffOn one_ne_zero NeZero.charZero_one WithTop.charZero ContMDiffOn.mdifferentiableOn Filter.mp_mem Iio_mem_nhds instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.univ_mem' Ioi_mem_nhds instClosedIicTopology
exists_lt_of_riemannianEDist_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder riemannianEDist	Real Real.instZero Real.instOne ContMDiffOn DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set.Icc Real.instPreorder pathELength	—	fact_one_le_two_ennreal riemannianEDist_def zero_le_one Real.instZeroLEOneClass Real.instIsOrderedRing Set.projIcc_left Path.source Set.projIcc_right Path.target LT.lt.le Fact.out contMDiffOn_comp_projIcc_iff ZeroLEOneClass.factZeroLtOne NeZero.charZero_one RCLike.charZero_rclike lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc
lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc 📖	mathematical	—	MeasureTheory.lintegral Set.Elem Real Set.Icc Real.instPreorder MeasureTheory.MeasureSpace.toMeasurableSpace MeasureTheory.Measure.Subtype.measureSpace Real.measureSpace Set Set.instMembership MeasureTheory.MeasureSpace.volume ENorm.enorm TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal EuclideanHalfSpace instTopologicalSpaceEuclideanHalfSpace modelWithCornersEuclideanHalfSpace instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instIccChartedSpace instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv instOneTangentSpaceRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc pathELength Set.projIcc Real.linearOrder LT.lt.le Fact.out Real.instLT	—	fact_one_le_two_ennreal LT.lt.le Fact.out pathELength_eq_lintegral_mfderivWithin_Icc MeasureTheory.measurePreserving_subtype_coe measurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.MeasurePreserving.lintegral_comp_emb MeasurableEmbedding.subtype_coe Set.projIcc_val
pathELength_add 📖	mathematical	Real Real.instLE	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring pathELength	—	Set.Icc_union_Ioc_eq_Icc pathELength_def MeasureTheory.lintegral_union measurableSet_Ioc BorelSpace.opensMeasurable Real.borelSpace instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Set.disjoint_iff_forall_ne LT.lt.ne LE.le.trans_lt MeasureTheory.restrict_Ioc_eq_restrict_Icc Real.noAtoms_volume
pathELength_comp_of_antitoneOn 📖	mathematical	ENormSMulClass Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace Real.instLE AntitoneOn Real.instPreorder Set.Icc DifferentiableOn Real.instAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace MDifferentiableOn Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf chartedSpaceSelf	pathELength	—	LE.le.eq_or_lt pathELength_self ContinuousOn.image_Icc_of_antitoneOn instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LT.lt.le DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology pathELength_eq_lintegral_mfderivWithin_Icc DifferentiableWithinAt.hasDerivWithinAt MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn measurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.setLIntegral_congr_fun RingHomCompTriple.ids mfderivWithin_comp Set.mem_image_of_mem mdifferentiableWithinAt_iff_differentiableWithinAt Set.subset_preimage_image uniqueMDiffWithinAt_iff_uniqueDiffWithinAt uniqueDiffOn_Icc mfderivWithin_eq_fderivWithin mul_one IsOrderedAddMonoid.toAddLeftMono AntitoneOn.derivWithin_nonpos map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass enorm_smul Real.enorm_of_nonneg enorm_neg
pathELength_comp_of_monotoneOn 📖	mathematical	ENormSMulClass Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace Real.instLE MonotoneOn Real.instPreorder Set.Icc DifferentiableOn Real.instAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace MDifferentiableOn Real.normedAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf chartedSpaceSelf	pathELength	—	LE.le.eq_or_lt pathELength_self ContinuousOn.image_Icc_of_monotoneOn instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing LT.lt.le DifferentiableOn.continuousOn IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology pathELength_eq_lintegral_mfderivWithin_Icc DifferentiableWithinAt.hasDerivWithinAt MeasureTheory.lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn measurableSet_Icc BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.setLIntegral_congr_fun RingHomCompTriple.ids mfderivWithin_comp Set.mem_image_of_mem mdifferentiableWithinAt_iff_differentiableWithinAt Set.subset_preimage_image uniqueMDiffWithinAt_iff_uniqueDiffWithinAt uniqueDiffOn_Icc mfderivWithin_eq_fderivWithin mul_one MonotoneOn.derivWithin_nonneg map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass enorm_smul Real.enorm_of_nonneg
pathELength_congr 📖	mathematical	Set.EqOn Real Set.Icc Real.instPreorder	pathELength	—	pathELength_congr_Ioo LT.lt.le
pathELength_congr_Ioo 📖	mathematical	Set.EqOn Real Set.Ioo Real.instPreorder	pathELength	—	pathELength_eq_lintegral_mfderiv_Ioo MeasureTheory.setLIntegral_congr_fun measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Filter.EventuallyEq.mfderiv_eq Filter.mp_mem Ioo_mem_nhds Filter.univ_mem'
pathELength_def 📖	mathematical	—	pathELength MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Icc Real.instPreorder ENorm.enorm TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv instOneTangentSpaceRealModelWithCornersSelf	—	—
pathELength_eq_lintegral_mfderivWithin_Icc 📖	mathematical	—	pathELength MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Icc Real.instPreorder ENorm.enorm TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderivWithin instOneTangentSpaceRealModelWithCornersSelf	—	pathELength_eq_lintegral_mfderiv_Icc MeasureTheory.restrict_Ioo_eq_restrict_Icc Real.noAtoms_volume MeasureTheory.setLIntegral_congr_fun measurableSet_Ioo BorelSpace.opensMeasurable Real.borelSpace HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid mfderivWithin_of_mem_nhds Icc_mem_nhds
pathELength_eq_lintegral_mfderiv_Icc 📖	mathematical	—	pathELength MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Icc Real.instPreorder ENorm.enorm TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv instOneTangentSpaceRealModelWithCornersSelf	—	pathELength_def
pathELength_eq_lintegral_mfderiv_Ioo 📖	mathematical	—	pathELength MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioo Real.instPreorder ENorm.enorm TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv instOneTangentSpaceRealModelWithCornersSelf	—	pathELength_eq_lintegral_mfderiv_Icc MeasureTheory.restrict_Ioo_eq_restrict_Icc Real.noAtoms_volume
pathELength_mono 📖	mathematical	Real Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder pathELength	—	pathELength_eq_lintegral_mfderiv_Icc MeasureTheory.lintegral_mono_set Set.Icc_subset_Icc
pathELength_self 📖	mathematical	—	pathELength ENNReal instZeroENNReal	—	pathELength_def IsScalarTower.right Set.Icc_self MeasureTheory.Measure.restrict_singleton MeasureTheory.NoAtoms.measure_singleton Real.noAtoms_volume zero_smul MeasureTheory.lintegral_zero_measure
riemannianEDist_comm 📖	mathematical	ENormSMulClass Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace	riemannianEDist	—	le_of_forall_gt exists_lt_locally_constant_of_riemannianEDist_lt zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike ContMDiff.comp ContDiff.neg contDiff_fun_id riemannianEDist_le_pathELength ContMDiff.contMDiffOn neg_neg neg_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LE.le.trans_lt pathELength_comp_of_antitoneOn zero_le_one Antitone.antitoneOn Monotone.neg covariant_swap_add_of_covariant_add monotone_id differentiableOn_neg ContMDiffOn.mdifferentiableOn one_ne_zero WithTop.charZero le_antisymm
riemannianEDist_def 📖	mathematical	—	riemannianEDist iInf ENNReal Path ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField EuclideanSpace PiLp.normedAddCommGroup instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal Fin.fintype Real.normedAddCommGroup PiLp.normedSpace NontriviallyNormedField.toNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal EuclideanHalfSpace instTopologicalSpaceEuclideanHalfSpace modelWithCornersEuclideanHalfSpace Set.Elem unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instChartedSpaceEuclideanHalfSpaceOfNatNatElemRealIcc WithTop ENat WithTop.one AddMonoidWithOne.toOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat DFunLike.coe Path.instFunLike MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace unitInterval.instMeasureSpaceElemReal MeasureTheory.MeasureSpace.volume ENorm.enorm TangentSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id instTopologicalSpaceTangentSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid instModuleTangentSpace ContinuousLinearMap.funLike mfderiv instOneTangentSpaceRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc Real.instZero Real.instOne	—	fact_one_le_two_ennreal
riemannianEDist_le_pathELength 📖	mathematical	ENormSMulClass Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace ContMDiffOn Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Set.Icc Real.instPreorder Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder riemannianEDist pathELength	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalAddTorsor.toContinuousVAdd instIsTopologicalAddTorsor_1 ContMDiffOn.comp contMDiffOn_iff_contDiffOn ContDiff.contDiffOn ContinuousAffineMap.contDiff Set.image_subset_iff ContinuousAffineMap.coe_lineMap_eq segment_eq_image_lineMap covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid segment_eq_Icc Real.instIsStrictOrderedRing Set.instReflSubset fact_one_le_two_ennreal LT.lt.le Fact.out contMDiffOn_comp_projIcc_iff ContMDiffOn.congr Set.projIcc_of_mem ContMDiff.continuous Real.instIsOrderedRing AffineMap.lineMap_apply_zero AffineMap.lineMap_apply_one riemannianEDist_def biInf_le LE.le.trans_eq lintegral_norm_mfderiv_Icc_eq_pathELength_projIcc zero_le_one Real.instZeroLEOneClass pathELength_congr pathELength_comp_of_monotoneOn Monotone.monotoneOn AffineMap.lineMap_mono PosSMulMono.toSMulPosMono IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule ContinuousAffineMap.differentiableOn ContMDiffOn.mdifferentiableOn one_ne_zero NeZero.charZero_one WithTop.charZero
riemannianEDist_self 📖	mathematical	ENormSMulClass Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace	riemannianEDist ENNReal instZeroENNReal	—	le_antisymm LE.le.trans_eq riemannianEDist_le_pathELength contMDiffOn_const le_rfl pathELength_self bot_eq_zero' ENNReal.instCanonicallyOrderedAdd bot_le
riemannianEDist_triangle 📖	mathematical	ENormSMulClass Real TangentSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid instTopologicalSpaceTangentSpace ENormedAddMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toENormedAddMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid instModuleTangentSpace	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder riemannianEDist Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	le_of_forall_gt ENNReal.exists_add_lt_of_add_lt exists_lt_locally_constant_of_riemannianEDist_lt zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Nat.instAtLeastTwoHAddOfNat one_lt_two IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid riemannianEDist_le_pathELength ContMDiff.contMDiffOn ContMDiff.piecewise_Iic Filter.EventuallyEq.trans Filter.EventuallyEq.symm Set.piecewise_eq_of_mem Set.piecewise_eq_of_notMem zero_le_two LE.le.trans_lt lt_trans pathELength_add zero_le_one one_le_two WithTop.add_lt_add NNReal.addLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add pathELength_congr pathELength_congr_Ioo

---

← Back to Index