Subpath

📁 Source: Mathlib/Topology/Subpath.lean

Statistics

Metric	Count
Definitions concat, concatSubpath, subpathTransSubpath, subpathTransSubpathRefl, concat, subpath, subpathAux	7
Theorems concat_hcomp, concat_one, concat_subpath, concat_two, concat_refl, concat_succ, concat_zero, range_subpath, range_subpathAux, range_subpath_of_ge, range_subpath_of_le, subpathAux_continuous, subpathAux_one, subpathAux_zero, subpath_continuous_family, subpath_self, subpath_zero_one, symm_subpath	18
Total	25

Path

Definitions

Name	Category	Theorems
concat 📖	CompOp	7 math math: Homotopic.concat_one, concat_zero, concat_succ, Homotopic.concat_hcomp, concat_refl, Homotopic.concat_subpath, Homotopic.concat_two
subpath 📖	CompOp	8 math math: subpath_self, range_subpath_of_ge, range_subpath, symm_subpath, subpath_continuous_family, subpath_zero_one, range_subpath_of_le, Homotopic.concat_subpath
subpathAux 📖	CompOp	4 math math: range_subpathAux, subpathAux_one, subpathAux_continuous, subpathAux_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concat_refl 📖	mathematical	—	concat refl	—	concat_zero concat_succ refl_trans_refl
concat_succ 📖	mathematical	—	concat trans	—	concat.eq_1
concat_zero 📖	mathematical	—	concat refl	—	concat.eq_1
range_subpath 📖	mathematical	—	Set.range Set.Elem Real unitInterval DFunLike.coe Path instFunLike subpath Set.image Set.uIcc Set.Icc.lattice Real.instZero Real.instOne Real.lattice	—	range_subpathAux Set.range_comp subpath.eq_1 coe_mk'
range_subpathAux 📖	mathematical	—	Set.range Set.Elem Real unitInterval subpathAux Set.uIcc Set.Icc.lattice Real.instZero Real.instOne Real.lattice	—	Set.range_eq_iff convex_uIcc Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing Set.left_mem_uIcc Set.right_mem_uIcc unitInterval.one_minus_nonneg unitInterval.nonneg sub_add_cancel segment_eq_image covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono segment_eq_uIcc
range_subpath_of_ge 📖	mathematical	Set.Elem Real unitInterval Real.instLE Set Set.instMembership	Set.range DFunLike.coe Path instFunLike subpath Set.image Set.Icc Subtype.preorder Real.instPreorder	—	range_subpath Set.uIcc_of_ge
range_subpath_of_le 📖	mathematical	Set.Elem Real unitInterval Real.instLE Set Set.instMembership	Set.range DFunLike.coe Path instFunLike subpath Set.image Set.Icc Subtype.preorder Real.instPreorder	—	range_subpath Set.uIcc_of_le
subpathAux_continuous 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace subpathAux	—	Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Continuous.fun_mul IsTopologicalSemiring.toContinuousMul Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const Continuous.comp' continuous_subtype_val Continuous.snd continuous_id' Continuous.fst
subpathAux_one 📖	mathematical	—	subpathAux Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing sub_self MulZeroClass.zero_mul one_mul zero_add Subtype.coe_eta
subpathAux_zero 📖	mathematical	—	subpathAux Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing sub_zero one_mul MulZeroClass.zero_mul add_zero Subtype.coe_eta
subpath_continuous_family 📖	mathematical	—	Continuous Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe Path instFunLike subpath	—	Continuous.comp' ContinuousMapClass.map_continuous continuousMapClass subpathAux_continuous
subpath_self 📖	mathematical	—	subpath refl DFunLike.coe Path Set.Elem Real unitInterval instFunLike	—	ext Distrib.rightDistribClass sub_add_cancel one_mul Subtype.coe_eta
subpath_zero_one 📖	mathematical	—	subpath Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne cast DFunLike.coe Path instFunLike source target	—	ext Real.instIsOrderedRing source target MulZeroClass.mul_zero mul_one zero_add Subtype.coe_eta
symm_subpath 📖	mathematical	—	symm DFunLike.coe Path Set.Elem Real unitInterval instFunLike subpath	—	ext sub_sub_cancel add_comm

Path.Homotopic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concat_hcomp 📖	mathematical	Path.Homotopic	Path.concat	—	—
concat_one 📖	mathematical	—	Path.Homotopic Path.concat	—	Path.concat_succ Path.concat_zero
concat_subpath 📖	mathematical	—	Path.Homotopic Set.Elem Real unitInterval DFunLike.coe Path Path.instFunLike Path.concat Path.subpath	—	—
concat_two 📖	mathematical	—	Path.Homotopic Path.concat Path.trans	—	Path.concat_succ Path.concat_zero hcomp refl

Path.Homotopy

Definitions

Name	Category	Theorems
concat 📖	CompOp	—
concatSubpath 📖	CompOp	—
subpathTransSubpath 📖	CompOp	—
subpathTransSubpathRefl 📖	CompOp	—

---

← Back to Index