Commit 2023-05-17 06:40 905ac032

View on Github →

feat: port AlgebraicTopology.FundamentalGroupoid.Basic (#3955)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

added theorem FundamentalGroupoid.comp_eq

added def FundamentalGroupoid.fromPath

added def FundamentalGroupoid.fromTop

added def FundamentalGroupoid.fundamentalGroupoidFunctor

added theorem FundamentalGroupoid.id_eq_path_refl

added theorem FundamentalGroupoid.map_eq

added def FundamentalGroupoid.toPath

added def FundamentalGroupoid.toTop

added def FundamentalGroupoid

added theorem Path.Homotopy.continuous_reflTransSymmAux

added theorem Path.Homotopy.continuous_transAssocReparamAux

added theorem Path.Homotopy.continuous_transReflReparamAux

added def Path.Homotopy.reflSymmTrans

added def Path.Homotopy.reflTrans

added def Path.Homotopy.reflTransSymm

added def Path.Homotopy.reflTransSymmAux

added theorem Path.Homotopy.reflTransSymmAux_mem_I

added def Path.Homotopy.transAssoc

added def Path.Homotopy.transAssocReparamAux

added theorem Path.Homotopy.transAssocReparamAux_mem_I

added theorem Path.Homotopy.transAssocReparamAux_one

added theorem Path.Homotopy.transAssocReparamAux_zero

added def Path.Homotopy.transRefl

added def Path.Homotopy.transReflReparamAux

added theorem Path.Homotopy.transReflReparamAux_mem_I

added theorem Path.Homotopy.transReflReparamAux_one

added theorem Path.Homotopy.transReflReparamAux_zero

added theorem Path.Homotopy.trans_assoc_reparam

added theorem Path.Homotopy.trans_refl_reparam