HomotopyGroup

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

Statistics

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

Cube

Definitions

Name	Category	Theorems
boundary 📖	CompOp	3 math math: GenLoop.homotopyTo_apply, boundary_sum_iff, insertAt_boundary
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
boundary_sum_iff 📖	mathematical	—	Set Set.instMembership boundary Set.Elem Real unitInterval	—	Real.instIsOrderedRing
insertAt_boundary 📖	mathematical	Set.Elem Real unitInterval Set.Icc.instZero Real.semiring Real.partialOrder Real.instIsOrderedRing Set.Icc.instOne Set Set.instMembership boundary	Set Set.instMembership boundary DFunLike.coe Homeomorph Set.Elem Real unitInterval 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	19 math math: fromLoop_apply, genLoopGenLoopEquiv_apply_coe, HomotopyGroup.isUnital_auxGroup, loopHomeo_apply, continuous_fromLoop, toLoop_apply, fromLoop_symm_toLoop, toLoop_apply_coe, loopHomeo_symm_apply, genLoopGenLoopEquiv_symm_apply_coe, HomotopyGroup.one_def, homotopyFrom_apply, const_apply, uncurry_apply, fromLoop_coe, homotopicTo, continuous_toLoop, fromLoop_trans_toLoop, apply_inl_apply_inr_eq_of_mem_boundary_sum
copy 📖	CompOp	2 math math: coe_copy, copy_eq
currySum 📖	CompOp	4 math math: currySum_apply_coe, continuous_currySum, genLoopGenLoopEquiv_symm_apply_coe, currySum_apply_inl_inr
fromLoop 📖	CompOp	7 math math: fromLoop_apply, to_from, continuous_fromLoop, fromLoop_symm_toLoop, loopHomeo_symm_apply, fromLoop_coe, fromLoop_trans_toLoop
genLoopGenLoopEquiv 📖	CompOp	2 math math: genLoopGenLoopEquiv_apply_coe, genLoopGenLoopEquiv_symm_apply_coe
homotopyFrom 📖	CompOp	1 math math: homotopyFrom_apply
homotopyTo 📖	CompOp	1 math math: homotopyTo_apply
inhabited 📖	CompOp	—
instFunLike 📖	CompOp	14 math math: fromLoop_apply, mk_apply, instContinuousEval, ext_iff, toLoop_apply, coe_coe, currySum_apply_inl_inr, coe_copy, boundary, homotopyFrom_apply, const_apply, uncurry_apply, instContinuousEvalConst, apply_inl_apply_inr_eq_of_mem_boundary_sum
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	5 math math: transAt_distrib, HomotopyGroup.genLoopEquivOfUnique_transAt, HomotopyGroup.transAt_indep, HomotopyGroup.mul_spec, fromLoop_trans_toLoop
uncurry 📖	CompOp	2 math math: genLoopGenLoopEquiv_apply_coe, uncurry_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_inl_apply_inr_eq_of_mem_boundary_sum 📖	mathematical	Set Set.instMembership Cube.boundary	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike ContinuousMap.compactOpen const	—	Cube.boundary_sum_iff
boundary 📖	mathematical	Set Set.instMembership Cube.boundary	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike	—	—
coe_coe 📖	mathematical	—	DFunLike.coe ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike 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	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_currySum 📖	mathematical	—	Continuous Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop ContinuousMap.compactOpen currySum	—	ContinuousMap.continuous_of_continuous_uncurry Continuous.eval instContinuousEval Continuous.fst continuous_id' Continuous.comp' Homeomorph.continuous Continuous.prodMk Continuous.snd
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
currySum_apply_coe 📖	mathematical	—	ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop DFunLike.coe ContinuousMap.compactOpen ContinuousMap.instFunLike currySum ContinuousMap.toFun ContinuousMap.curry ContinuousMap.comp instTopologicalSpaceProd Equiv.invFun Homeomorph.toEquiv Homeomorph.sumArrowHomeomorphProdArrow	—	—
currySum_apply_inl_inr 📖	mathematical	—	DFunLike.coe Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop instFunLike ContinuousMap.compactOpen ContinuousMap.instFunLike currySum	—	—
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
genLoopGenLoopEquiv_apply_coe 📖	mathematical	—	ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop DFunLike.coe Homeomorph ContinuousMap.compactOpen const EquivLike.toFunLike Homeomorph.instEquivLike genLoopGenLoopEquiv ContinuousMap.comp instTopologicalSpaceProd uncurry Equiv.toFun Homeomorph.toEquiv Homeomorph.sumArrowHomeomorphProdArrow	—	—
genLoopGenLoopEquiv_symm_apply_coe 📖	mathematical	—	ContinuousMap Set.Elem Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop ContinuousMap.compactOpen const DFunLike.coe Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm genLoopGenLoopEquiv currySum	—	—
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 instFunLike 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 ContinuousMap Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop 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
uncurry_apply 📖	mathematical	—	DFunLike.coe ContinuousMap instTopologicalSpaceProd Pi.topologicalSpace Set.Elem Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousMap.instFunLike uncurry GenLoop instFunLike ContinuousMap.compactOpen const	—	—

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
homotopyGroupOfUniqueMulEquivFundamentalGroup 📖	CompOp	—
pi0EquivZerothHomotopy 📖	CompOp	—
pi1EquivFundamentalGroup 📖	CompOp	—
pi1MulEquivFundamentalGroup 📖	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
genLoopEquivOfUnique_transAt 📖	mathematical	—	DFunLike.coe Equiv Set.Elem ContinuousMap Pi.topologicalSpace Real unitInterval instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace GenLoop LoopSpace EquivLike.toFunLike Equiv.instEquivLike genLoopEquivOfUnique GenLoop.transAt Unique.instInhabited Path.trans	—	Path.ext one_div Real.instIsOrderedRing Unique.eq_default Function.update_self
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	36 math math: GenLoop.fromLoop_apply, HomotopyGroup.symmAt_indep, GenLoop.homotopyTo_apply, GenLoop.genLoopGenLoopEquiv_apply_coe, HomotopyGroup.isUnital_auxGroup, GenLoop.loopHomeo_apply, HomotopyGroup.genLoopEquivOfUnique_transAt, GenLoop.mk_apply, HomotopyGroup.transAt_indep, GenLoop.instContinuousEval, GenLoop.currySum_apply_coe, GenLoop.ext_iff, GenLoop.continuous_currySum, GenLoop.continuous_fromLoop, GenLoop.toLoop_apply, HomotopyGroup.mul_spec, GenLoop.fromLoop_symm_toLoop, GenLoop.coe_coe, GenLoop.toLoop_apply_coe, GenLoop.loopHomeo_symm_apply, GenLoop.genLoopGenLoopEquiv_symm_apply_coe, HomotopyGroup.one_def, HomotopyGroup.inv_spec, GenLoop.currySum_apply_inl_inr, GenLoop.Homotopic.equiv, GenLoop.coe_copy, GenLoop.boundary, GenLoop.homotopyFrom_apply, GenLoop.const_apply, GenLoop.uncurry_apply, GenLoop.fromLoop_coe, GenLoop.homotopicTo, GenLoop.continuous_toLoop, GenLoop.fromLoop_trans_toLoop, GenLoop.instContinuousEvalConst, GenLoop.apply_inl_apply_inr_eq_of_mem_boundary_sum
HomotopyGroup 📖	CompOp	3 math math: HomotopyGroup.isUnital_auxGroup, HomotopyGroup.one_def, HomotopyGroup.inv_spec
LoopSpace 📖	CompOp	7 math math: GenLoop.fromLoop_apply, GenLoop.loopHomeo_apply, HomotopyGroup.genLoopEquivOfUnique_transAt, GenLoop.continuous_fromLoop, GenLoop.toLoop_apply, GenLoop.loopHomeo_symm_apply, GenLoop.continuous_toLoop
genLoopEquivOfUnique 📖	CompOp	1 math math: HomotopyGroup.genLoopEquivOfUnique_transAt
genLoopHomeoOfIsEmpty 📖	CompOp	—
homotopyGroupEquivFundamentalGroup 📖	CompOp	—
homotopyGroupEquivFundamentalGroupOfUnique 📖	CompOp	—
homotopyGroupEquivZerothHomotopyOfIsEmpty 📖	CompOp	—
instInhabitedHomotopyGroup 📖	CompOp	—

---

← Back to Index