HomotopyGroup

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

Statistics

Metric	Count
Definitions boundary, insertAt, splitAt, GenLoop, Homotopic, setoid, cCompInsert, const, copy, fromLoop, homotopyFrom, homotopyTo, inhabited, instFunLike, loopHomeo, symmAt, toLoop, transAt, HomotopyGroup, auxGroup, commGroup, group, pi0EquivZerothHomotopy, pi1EquivFundamentalGroup, LoopSpace, inhabited, termΩ, «termΩ^», termπ_, «termI^_», genLoopEquivOfUnique, genLoopHomeoOfIsEmpty, homotopyGroupEquivFundamentalGroup, homotopyGroupEquivFundamentalGroupOfUnique, homotopyGroupEquivZerothHomotopyOfIsEmpty, instInhabitedHomotopyGroup	36
Theorems insertAt_boundary, equiv, refl, trans, boundary, coe_copy, const_apply, continuous_fromLoop, continuous_toLoop, copy_eq, ext, ext_iff, fromLoop_apply, fromLoop_coe, fromLoop_symm_toLoop, fromLoop_trans_toLoop, homotopicFrom, homotopicTo, homotopyFrom_apply, homotopyTo_apply, instContinuousEval, instContinuousEvalConst, loopHomeo_apply, loopHomeo_symm_apply, mk_apply, toLoop_apply, toLoop_apply_coe, to_from, transAt_distrib, auxGroup_indep, inv_spec, isUnital_auxGroup, mul_spec, one_def, symmAt_indep, transAt_indep	36
Total	72

Cube

Definitions

Name	Category	Theorems
boundary 📖	CompOp	1 math math: GenLoop.homotopyTo_apply
insertAt 📖	CompOp	4 math math: GenLoop.homotopyTo_apply, GenLoop.toLoop_apply, GenLoop.toLoop_apply_coe, insertAt_boundary
splitAt 📖	CompOp	3 math math: GenLoop.fromLoop_apply, GenLoop.homotopyFrom_apply, GenLoop.fromLoop_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
insertAt_boundary 📖	mathematical	Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne Set Set.instMembership boundary	DFunLike.coe Homeomorph instTopologicalSpaceProd instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.topologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike insertAt	—	Real.instIsOrderedRing Homeomorph.funSplitAt_symm_apply Subtype.prop Subtype.coe_eta

GenLoop

Definitions

Name	Category	Theorems
Homotopic 📖	MathDef	5 math math: Homotopic.trans, Homotopic.symm, homotopicFrom, Homotopic.refl, Homotopic.equiv
cCompInsert 📖	CompOp	—
const 📖	CompOp	15 math math: fromLoop_apply, HomotopyGroup.isUnital_auxGroup, loopHomeo_apply, continuous_fromLoop, toLoop_apply, fromLoop_symm_toLoop, toLoop_apply_coe, loopHomeo_symm_apply, HomotopyGroup.one_def, homotopyFrom_apply, const_apply, fromLoop_coe, homotopicTo, continuous_toLoop, fromLoop_trans_toLoop
copy 📖	CompOp	2 math math: coe_copy, copy_eq
fromLoop 📖	CompOp	7 math math: fromLoop_apply, to_from, continuous_fromLoop, fromLoop_symm_toLoop, loopHomeo_symm_apply, fromLoop_coe, fromLoop_trans_toLoop
homotopyFrom 📖	CompOp	1 math math: homotopyFrom_apply
homotopyTo 📖	CompOp	1 math math: homotopyTo_apply
inhabited 📖	CompOp	—
instFunLike 📖	CompOp	8 math math: fromLoop_apply, mk_apply, instContinuousEval, ext_iff, toLoop_apply, boundary, const_apply, instContinuousEvalConst
loopHomeo 📖	CompOp	2 math math: loopHomeo_apply, loopHomeo_symm_apply
symmAt 📖	CompOp	3 math math: HomotopyGroup.symmAt_indep, fromLoop_symm_toLoop, HomotopyGroup.inv_spec
toLoop 📖	CompOp	9 math math: loopHomeo_apply, to_from, toLoop_apply, fromLoop_symm_toLoop, toLoop_apply_coe, homotopyFrom_apply, homotopicTo, continuous_toLoop, fromLoop_trans_toLoop
transAt 📖	CompOp	4 math math: transAt_distrib, HomotopyGroup.transAt_indep, HomotopyGroup.mul_spec, fromLoop_trans_toLoop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boundary 📖	mathematical	Set Set.instMembership Cube.boundary	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike	—	—
coe_copy 📖	mathematical	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike	copy	—	—
const_apply 📖	mathematical	—	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike const	—	—
continuous_fromLoop 📖	mathematical	—	Continuous LoopSpace Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop ContinuousMap.compactOpen const Path.instTopologicalSpace fromLoop	—	Continuous.comp ContinuousMap.continuous_precomp ContinuousMap.continuous_uncurry locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal ContinuousMap.continuous_postcomp continuous_induced_dom
continuous_toLoop 📖	mathematical	—	Continuous Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop LoopSpace ContinuousMap.compactOpen const Path.instTopologicalSpace toLoop	—	Path.continuous_uncurry_iff Continuous.comp ContinuousEval.continuous_eval ContinuousMap.instContinuousEvalOfLocallyCompactPair instLocallyCompactPairOfLocallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Continuous.prodMap ContinuousMap.continuous_curry Prod.locallyCompactSpace Function.locallyCompactSpace ContinuousMap.continuous_precomp continuous_subtype_val continuous_id
copy_eq 📖	mathematical	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike	copy	—	ext
ext 📖	—	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike	—	—	DFunLike.coe_injective'
ext_iff 📖	mathematical	—	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike	—	ext
fromLoop_apply 📖	mathematical	—	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike fromLoop LoopSpace ContinuousMap.compactOpen const Path.instFunLike Homeomorph instTopologicalSpaceProd EquivLike.toFunLike Homeomorph.instEquivLike Cube.splitAt	—	—
fromLoop_coe 📖	mathematical	—	ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop fromLoop ContinuousMap.comp instTopologicalSpaceProd ContinuousMap.uncurry ContinuousMap.compactOpen Path.toContinuousMap const toContinuousMap Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Cube.splitAt	—	—
fromLoop_symm_toLoop 📖	mathematical	—	fromLoop Path.symm Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop ContinuousMap.compactOpen const toLoop symmAt	—	copy_eq
fromLoop_trans_toLoop 📖	mathematical	—	fromLoop Path.trans Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop ContinuousMap.compactOpen const toLoop transAt	—	copy_eq
homotopicFrom 📖	mathematical	—	Homotopic	—	Nonempty.map Real.instIsOrderedRing homotopyFrom_apply ContinuousMap.HomotopyWith.apply_zero Equiv.left_inv ContinuousMap.HomotopyWith.apply_one Continuous.comp ContinuousMap.continuous_toFun eq_or_ne ContinuousMap.HomotopyRel.eq_fst boundary
homotopicTo 📖	mathematical	—	Path.Homotopic Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop ContinuousMap.compactOpen const toLoop	—	Nonempty.map Real.instIsOrderedRing homotopyTo_apply ContinuousMap.HomotopyRel.eq_fst Cube.insertAt_boundary ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass ext toLoop_apply ContinuousMap.HomotopyWith.apply_zero ContinuousMap.HomotopyWith.apply_one Continuous.comp ContinuousMap.continuous_toFun Homeomorph.funSplitAt_symm_apply
homotopyFrom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap Set.Elem Real unitInterval instTopologicalSpaceProd instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Pi.topologicalSpace ContinuousMap.instFunLike homotopyFrom GenLoop ContinuousMap.HomotopyWith ContinuousMap.compactOpen Path.toContinuousMap const toLoop ContinuousMap.HomotopyWith.instFunLike Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Cube.splitAt	—	—
homotopyTo_apply 📖	mathematical	—	DFunLike.coe ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike instTopologicalSpaceProd ContinuousMap.compactOpen homotopyTo ContinuousMap.HomotopyRel GenLoop Cube.boundary ContinuousMap.HomotopyWith.instFunLike Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Cube.insertAt	—	—
instContinuousEval 📖	mathematical	—	ContinuousEval Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike ContinuousMap.compactOpen	—	ContinuousEval.of_continuous_forget ContinuousMap.instContinuousEvalOfLocallyCompactPair instLocallyCompactPairOfLocallyCompactSpace Function.locallyCompactSpace locallyCompact_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal continuous_subtype_val
instContinuousEvalConst 📖	mathematical	—	ContinuousEvalConst Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike ContinuousMap.compactOpen	—	ContinuousEval.toContinuousEvalConst instContinuousEval
loopHomeo_apply 📖	mathematical	—	DFunLike.coe Homeomorph Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop LoopSpace ContinuousMap.compactOpen const Path.instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike loopHomeo toLoop	—	—
loopHomeo_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph LoopSpace Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop ContinuousMap.compactOpen const Path.instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm loopHomeo fromLoop	—	—
mk_apply 📖	mathematical	ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop	DFunLike.coe instFunLike ContinuousMap.instFunLike	—	—
toLoop_apply 📖	mathematical	—	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike LoopSpace ContinuousMap.compactOpen const Path.instFunLike toLoop Homeomorph instTopologicalSpaceProd EquivLike.toFunLike Homeomorph.instEquivLike Cube.insertAt	—	—
toLoop_apply_coe 📖	mathematical	—	ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop DFunLike.coe Path ContinuousMap.compactOpen const Path.instFunLike toLoop ContinuousMap.instFunLike ContinuousMap.curry ContinuousMap.comp instTopologicalSpaceProd toContinuousMap Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Cube.insertAt	—	—
to_from 📖	mathematical	—	toLoop fromLoop	—	Real.instIsOrderedRing Homeomorph.toContinuousMap_comp_symm ContinuousMap.comp_id Path.ext ext
transAt_distrib 📖	mathematical	—	transAt	—	ext copy.congr_simp Function.update_apply Set.projIcc.congr_simp ite_ite_comm

GenLoop.Homotopic

Definitions

Name	Category	Theorems
setoid 📖	CompOp	6 math math: HomotopyGroup.symmAt_indep, HomotopyGroup.isUnital_auxGroup, HomotopyGroup.transAt_indep, HomotopyGroup.mul_spec, HomotopyGroup.one_def, HomotopyGroup.inv_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv 📖	mathematical	—	Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop GenLoop.Homotopic	—	refl symm trans
refl 📖	mathematical	—	GenLoop.Homotopic	—	ContinuousMap.HomotopicRel.refl
trans 📖	mathematical	—	GenLoop.Homotopic	—	ContinuousMap.HomotopicRel.trans

HomotopyGroup

Definitions

Name	Category	Theorems
auxGroup 📖	CompOp	2 math math: auxGroup_indep, isUnital_auxGroup
commGroup 📖	CompOp	—
group 📖	CompOp	2 math math: one_def, inv_spec
pi0EquivZerothHomotopy 📖	CompOp	—
pi1EquivFundamentalGroup 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
auxGroup_indep 📖	mathematical	—	auxGroup	—	Group.ext EckmannHilton.mul isUnital_auxGroup GenLoop.fromLoop_trans_toLoop GenLoop.transAt_distrib
inv_spec 📖	mathematical	—	HomotopyGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid group Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop GenLoop.Homotopic.setoid GenLoop.symmAt	—	symmAt_indep GenLoop.fromLoop_symm_toLoop
isUnital_auxGroup 📖	mathematical	—	EckmannHilton.IsUnital HomotopyGroup Semigroup.toMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid auxGroup Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop GenLoop.Homotopic.setoid GenLoop.const	—	Monoid.one_mul Monoid.mul_one
mul_spec 📖	mathematical	—	Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop GenLoop.Homotopic.setoid GenLoop.transAt	—	transAt_indep GenLoop.fromLoop_trans_toLoop
one_def 📖	mathematical	—	HomotopyGroup InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid group Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop GenLoop.Homotopic.setoid GenLoop.const	—	—
symmAt_indep 📖	mathematical	—	Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop GenLoop.Homotopic.setoid GenLoop.symmAt	—	auxGroup_indep
transAt_indep 📖	mathematical	—	Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop GenLoop.Homotopic.setoid GenLoop.transAt	—	auxGroup_indep

LoopSpace

Definitions

Name	Category	Theorems
inhabited 📖	CompOp	—

Topology

Definitions

Name	Category	Theorems
termπ_ 📖	CompOp	—
«termI^_» 📖	CompOp	—

Topology.Homotopy

Definitions

Name	Category	Theorems
termΩ 📖	CompOp	—
«termΩ^» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
GenLoop 📖	CompOp	25 math math: GenLoop.fromLoop_apply, HomotopyGroup.symmAt_indep, GenLoop.homotopyTo_apply, HomotopyGroup.isUnital_auxGroup, GenLoop.loopHomeo_apply, HomotopyGroup.transAt_indep, GenLoop.instContinuousEval, GenLoop.ext_iff, GenLoop.continuous_fromLoop, GenLoop.toLoop_apply, HomotopyGroup.mul_spec, GenLoop.fromLoop_symm_toLoop, GenLoop.toLoop_apply_coe, GenLoop.loopHomeo_symm_apply, HomotopyGroup.one_def, HomotopyGroup.inv_spec, GenLoop.Homotopic.equiv, GenLoop.boundary, GenLoop.homotopyFrom_apply, GenLoop.const_apply, GenLoop.fromLoop_coe, GenLoop.homotopicTo, GenLoop.continuous_toLoop, GenLoop.fromLoop_trans_toLoop, GenLoop.instContinuousEvalConst
HomotopyGroup 📖	CompOp	3 math math: HomotopyGroup.isUnital_auxGroup, HomotopyGroup.one_def, HomotopyGroup.inv_spec
LoopSpace 📖	CompOp	6 math math: GenLoop.fromLoop_apply, GenLoop.loopHomeo_apply, GenLoop.continuous_fromLoop, GenLoop.toLoop_apply, GenLoop.loopHomeo_symm_apply, GenLoop.continuous_toLoop
genLoopEquivOfUnique 📖	CompOp	—
genLoopHomeoOfIsEmpty 📖	CompOp	—
homotopyGroupEquivFundamentalGroup 📖	CompOp	—
homotopyGroupEquivFundamentalGroupOfUnique 📖	CompOp	—
homotopyGroupEquivZerothHomotopyOfIsEmpty 📖	CompOp	—
instInhabitedHomotopyGroup 📖	CompOp	—

---

← Back to Index