Path

📁 Source: Mathlib/Topology/Homotopy/Path.lean

Statistics

Metric	Count
Definitions evalAt, Homotopic, cast, comp, map, mapFn, mk, refl, trans, instInhabitedQuotientUnitUnit, setoid, cast, eval, hcomp, map, pathCast, refl, reparam, symm₂, trans, toHomotopyConst	21
Theorems evalAt_apply, pathExtend_evalAt, homotopic_const_iff, cast_cast, cast_rfl_rfl, eq, exact, ind, ind₂, mk''_eq_mk, mk'_eq_mk, mk_cast, mk_map, mk_refl, mk_surjective, mk_symm, mk_trans, comp_lift, equivalence, hcomp, hpath_hext, instIsEquiv, map, map_lift, pathCast, refl, symm₂, trans, cast_apply, coeFn_injective, eval_apply, eval_one, eval_zero, hcomp_apply, hcomp_half, map_apply, refl_apply, source, symm_apply, symm_bijective, symm_symm, symm_trans, symm₂_apply, target, trans_apply, toHomotopyConst_apply	46
Total	67

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homotopic_const_iff 📖	mathematical	—	Homotopic const Joined	—	Real.instIsOrderedRing Homotopy.apply_zero Homotopy.apply_one

ContinuousMap.Homotopy

Definitions

Name	Category	Theorems
evalAt 📖	CompOp	9 math math: curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt, evalAt_eq, pathExtend_evalAt, curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable, Path.Homotopic.map_trans_evalAt, evalAt_apply, curveIntegral_add_curveIntegral_eq_of_diffContOnCl, evalAt_affine, eq_diag_path

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
evalAt_apply 📖	mathematical	—	DFunLike.coe Path ContinuousMap ContinuousMap.instFunLike Set.Elem Real unitInterval Path.instFunLike evalAt ContinuousMap.Homotopy instFunLike	—	—
pathExtend_evalAt 📖	mathematical	—	DFunLike.coe ContinuousMap Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike Path.extend evalAt ContinuousMap.compactOpen extend	—	—

Path

Definitions

Name	Category	Theorems
Homotopic 📖	MathDef	25 math math: Homotopic.trans, Homotopic.trans_assoc, Homotopic.pathCast, Homotopic.symm, Homotopic.concat_one, Homotopic.trans_symm, Homotopic.symm₂, Homotopic.map, Homotopic.map_trans_evalAt, Homotopic.refl, Homotopic.refl_trans, SimplyConnectedSpace.paths_homotopic, Homotopic.Quotient.exact, Homotopic.Quotient.eq, Homotopic.trans_refl, Homotopic.symm_trans, Homotopic.hcomp, FundamentalGroupoid.fromPath_eq_iff_homotopic, simply_connected_iff_loops_nullhomotopic, simply_connected_iff_paths_homotopic', GenLoop.homotopicTo, Homotopic.instIsEquiv, Homotopic.concat_subpath, Homotopic.concat_two, Homotopic.equivalence
toHomotopyConst 📖	CompOp	1 math math: toHomotopyConst_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toHomotopyConst_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.Homotopy ContinuousMap.const Set.Elem Real unitInterval ContinuousMap.Homotopy.instFunLike toHomotopyConst Path instFunLike	—	—

Path.Homotopic

Definitions

Name	Category	Theorems
instInhabitedQuotientUnitUnit 📖	CompOp	—
setoid 📖	CompOp	9 math math: FundamentalGroupoid.eqToHom_eq, ContinuousMap.Homotopy.evalAt_eq, ContinuousMap.Homotopy.heq_path_of_eq_image, Quotient.mk'_eq_mk, ContinuousMap.Homotopy.eq_path_of_eq_image, Quotient.mk''_eq_mk, FundamentalGroupoid.id_eq_path_refl, ContinuousMap.Homotopy.eq_diag_path, hpath_hext

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_lift 📖	mathematical	—	Path.trans Quotient.trans	—	Quotient.mk_trans
equivalence 📖	mathematical	—	Path Path.Homotopic	—	refl symm trans
hcomp 📖	mathematical	—	Path.Homotopic Path.trans	—	Nonempty.map2
hpath_hext 📖	mathematical	DFunLike.coe Path Set.Elem Real unitInterval Path.instFunLike	Quotient setoid	—	Path.ext Real.instIsOrderedRing Path.target Path.source
instIsEquiv 📖	mathematical	—	IsEquiv Path Path.Homotopic	—	refl trans symm
map 📖	mathematical	—	Path.Homotopic DFunLike.coe ContinuousMap ContinuousMap.instFunLike Path.map ContinuousMap.continuous	—	Nonempty.map ContinuousMap.continuous
map_lift 📖	mathematical	—	DFunLike.coe ContinuousMap ContinuousMap.instFunLike Path.map ContinuousMap.continuous Quotient.map	—	Quotient.mk_map
pathCast 📖	mathematical	—	Path.Homotopic Path.cast	—	—
refl 📖	mathematical	—	Path.Homotopic	—	—
symm₂ 📖	mathematical	—	Path.Homotopic Path.symm	—	Nonempty.map
trans 📖	mathematical	—	Path.Homotopic	—	Nonempty.map2

Path.Homotopic.Quotient

Definitions

Name	Category	Theorems
cast 📖	CompOp	3 math math: cast_rfl_rfl, cast_cast, mk_cast
comp 📖	CompOp	—
map 📖	CompOp	8 math math: Path.Homotopic.map_lift, FundamentalGroupoid.map_map, FundamentalGroup.map_apply, IsCoveringMap.injective_path_homotopic_map, IsCoveringMap.injective_path_homotopic_mapFn, IsCoveringMap.monodromy_map, mk_map, FundamentalGroupoid.map_eq
mapFn 📖	CompOp	—
mk 📖	CompOp	—
refl 📖	CompOp	6 math math: trans_symm, refl_trans, trans_refl, IsCoveringMap.monodromy_refl, symm_trans, mk_refl
trans 📖	CompOp	11 math math: trans_symm, Path.Homotopic.comp_pi_eq_pi_comp, Path.Homotopic.comp_lift, refl_trans, FundamentalGroupoid.comp_eq, trans_refl, IsCoveringMap.monodromy_trans_apply, mk_trans, symm_trans, Path.Homotopic.comp_prod_eq_prod_comp, trans_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_cast 📖	mathematical	—	cast	—	ind
cast_rfl_rfl 📖	mathematical	—	cast	—	ind
eq 📖	mathematical	—	Path.Homotopic	—	Quotient.eq
exact 📖	mathematical	—	Path.Homotopic	—	—
ind 📖	—	—	—	—	—
ind₂ 📖	—	—	—	—	—
mk''_eq_mk 📖	mathematical	—	Quotient.mk'' Path Path.Homotopic.setoid	—	—
mk'_eq_mk 📖	mathematical	—	Path Path.Homotopic.setoid	—	—
mk_cast 📖	mathematical	—	Path.cast cast	—	—
mk_map 📖	mathematical	—	DFunLike.coe ContinuousMap ContinuousMap.instFunLike Path.map ContinuousMap.continuous map	—	ContinuousMap.continuous
mk_refl 📖	mathematical	—	Path.refl refl	—	—
mk_surjective 📖	mathematical	—	Path Path.Homotopic.Quotient	—	Quotient.mk'_surjective
mk_symm 📖	mathematical	—	Path.symm symm	—	—
mk_trans 📖	mathematical	—	Path.trans trans	—	—

Path.Homotopy

Definitions

Name	Category	Theorems
cast 📖	CompOp	1 math math: cast_apply
eval 📖	CompOp	4 math math: eval_zero, hcomp_apply, eval_apply, eval_one
hcomp 📖	CompOp	2 math math: hcomp_half, hcomp_apply
map 📖	CompOp	1 math math: map_apply
pathCast 📖	CompOp	—
refl 📖	CompOp	1 math math: refl_apply
reparam 📖	CompOp	—
symm₂ 📖	CompOp	1 math math: symm₂_apply
trans 📖	CompOp	2 math math: symm_trans, trans_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cast_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap ContinuousMap.HomotopyWith.instFunLike cast	—	Real.instIsOrderedRing
coeFn_injective 📖	mathematical	—	Path.Homotopy DFunLike.coe Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap	—	DFunLike.coe_injective Real.instIsOrderedRing
eval_apply 📖	mathematical	—	DFunLike.coe Path Set.Elem Real unitInterval Path.instFunLike eval ContinuousMap instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike ContinuousMap.compactOpen ContinuousMap.Homotopy.curry Path.toContinuousMap ContinuousMap.HomotopyWith.toHomotopy	—	—
eval_one 📖	mathematical	—	eval Set.Elem Real unitInterval Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Path.ext Real.instIsOrderedRing ContinuousMap.Homotopy.curry_one
eval_zero 📖	mathematical	—	eval Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Path.ext Real.instIsOrderedRing ContinuousMap.Homotopy.curry_zero
hcomp_apply 📖	mathematical	—	DFunLike.coe Path.Homotopy Path.trans Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap hcomp Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.decidableLE Path Path.instFunLike eval Real.instMul AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Set.Icc Real.instPreorder Real.instZero unitInterval.mul_pos_mem_iff zero_lt_two Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Ring.toSemiring Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instIsOrderedAddMonoid Preorder.toLE Real.instSub unitInterval.two_mul_sub_one_mem_iff LT.lt.le PartialOrder.toPreorder LinearOrder.toPartialOrder Real.linearOrder Preorder.toLT not_le	—	Nat.instAtLeastTwoHAddOfNat unitInterval.mul_pos_mem_iff zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid unitInterval.two_mul_sub_one_mem_iff LT.lt.le not_le Path.extend_apply
hcomp_half 📖	mathematical	—	DFunLike.coe Path.Homotopy Path.trans Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap hcomp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Preorder.toLE Real.instPreorder Real.instZero	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.isRat_le_true Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_le_true Real.instIsOrderedRing Nat.cast_zero Mathlib.Meta.NormNum.IsNNRat.to_isNat Path.extend_apply Path.target Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.IsNat.to_isInt Path.source
map_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap ContinuousMap ContinuousMap.instFunLike Path.map ContinuousMap.continuous ContinuousMap.HomotopyWith.instFunLike map Path.Homotopy	—	ContinuousMap.continuous Real.instIsOrderedRing
refl_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap ContinuousMap.HomotopyWith.instFunLike refl Path Path.instFunLike	—	Real.instIsOrderedRing
source 📖	mathematical	—	DFunLike.coe Path.Homotopy Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing ContinuousMap.HomotopyRel.eq_fst Path.source
symm_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap ContinuousMap.HomotopyWith.instFunLike symm unitInterval.symm	—	Real.instIsOrderedRing
symm_bijective 📖	mathematical	—	Function.Bijective Path.Homotopy symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	ContinuousMap.HomotopyRel.symm_symm Real.instIsOrderedRing
symm_trans 📖	mathematical	—	symm trans	—	ContinuousMap.HomotopyRel.symm_trans Real.instIsOrderedRing
symm₂_apply 📖	mathematical	—	DFunLike.coe ContinuousMap.HomotopyWith Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap Path.symm ContinuousMap.HomotopyWith.instFunLike symm₂ Path.Homotopy unitInterval.symm	—	Real.instIsOrderedRing
target 📖	mathematical	—	DFunLike.coe Path.Homotopy Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap Set.Icc.instOne Real.semiring Real.partialOrder Real.instIsOrderedRing	—	Real.instIsOrderedRing ContinuousMap.HomotopyRel.eq_fst Path.target
trans_apply 📖	mathematical	—	DFunLike.coe Path.Homotopy Set.Elem Real unitInterval ContinuousMap.HomotopyWith.instFunLike instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Path.toContinuousMap trans Real.instLE DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.decidableLE Real.instMul AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Set.Icc Real.instPreorder Real.instZero unitInterval.mul_pos_mem_iff zero_lt_two Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero Ring.toSemiring Real.instIsStrictOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instIsOrderedAddMonoid Preorder.toLE Real.instSub unitInterval.two_mul_sub_one_mem_iff LT.lt.le PartialOrder.toPreorder LinearOrder.toPartialOrder Real.linearOrder Preorder.toLT not_le	—	ContinuousMap.HomotopyRel.trans_apply Real.instIsOrderedRing

---

← Back to Index