Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-17 11:01 5eb47c00

View on Github →

feat(topology/homotopy): Define the fundamental groupoid of a topological space (#9683)

Estimated changes

Modified src/topology/homotopy/basic.lean

added def continuous_map.homotopy.cast

added def continuous_map.homotopy_rel.cast

added def continuous_map.homotopy_with.cast

Created src/topology/homotopy/fundamental_groupoid.lean

added def fundamental_groupoid

added theorem path.homotopy.continuous_refl_trans_symm_aux

added theorem path.homotopy.continuous_trans_assoc_reparam_aux

added theorem path.homotopy.continuous_trans_refl_reparam_aux

added def path.homotopy.refl_symm_trans

added def path.homotopy.refl_trans

added def path.homotopy.refl_trans_symm

added def path.homotopy.refl_trans_symm_aux

added theorem path.homotopy.refl_trans_symm_aux_mem_I

added def path.homotopy.trans_assoc

added theorem path.homotopy.trans_assoc_reparam

added def path.homotopy.trans_assoc_reparam_aux

added theorem path.homotopy.trans_assoc_reparam_aux_mem_I

added theorem path.homotopy.trans_assoc_reparam_aux_one

added theorem path.homotopy.trans_assoc_reparam_aux_zero

added def path.homotopy.trans_refl

added theorem path.homotopy.trans_refl_reparam

added def path.homotopy.trans_refl_reparam_aux

added theorem path.homotopy.trans_refl_reparam_aux_mem_I

added theorem path.homotopy.trans_refl_reparam_aux_one

added theorem path.homotopy.trans_refl_reparam_aux_zero

Modified src/topology/homotopy/path.lean

added def path.homotopy.cast

added def path.homotopy.reparam

added def path.homotopy.symm₂

Modified src/topology/path_connected.lean

added theorem path.symm_symm

added theorem path.trans_apply

added theorem path.trans_symm