Commit 2023-07-07 11:12 e5bc4385

View on Github →

feat: port AlgebraicTopology.FundamentalGroupoid.InducedMaps (#5756)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

added theorem ContinuousMap.Homotopy.apply_one_path

added theorem ContinuousMap.Homotopy.apply_zero_path

added def ContinuousMap.Homotopy.diagonalPath'

added def ContinuousMap.Homotopy.diagonalPath

added theorem ContinuousMap.Homotopy.eq_diag_path

added theorem ContinuousMap.Homotopy.eq_path_of_eq_image

added theorem ContinuousMap.Homotopy.evalAt_eq

added theorem ContinuousMap.Homotopy.hcast_def

added theorem ContinuousMap.Homotopy.heq_path_of_eq_image

added def ContinuousMap.Homotopy.uliftMap

added theorem ContinuousMap.Homotopy.ulift_apply

added def FundamentalGroupoidFunctor.equivOfHomotopyEquiv

added def FundamentalGroupoidFunctor.homotopicMapsNatIso

added def unitInterval.path01

added def unitInterval.uhpath01

added def unitInterval.upath01

Modified Mathlib/CategoryTheory/EqToHom.lean

deleted theorem CategoryTheory.Functor.conj_eqToHom_iff_hEq

added theorem CategoryTheory.Functor.conj_eqToHom_iff_heq

deleted theorem CategoryTheory.Functor.map_comp_hEq'

deleted theorem CategoryTheory.Functor.map_comp_hEq

added theorem CategoryTheory.Functor.map_comp_heq'

added theorem CategoryTheory.Functor.map_comp_heq

deleted theorem CategoryTheory.Functor.postcomp_map_hEq'

deleted theorem CategoryTheory.Functor.postcomp_map_hEq

added theorem CategoryTheory.Functor.postcomp_map_heq'

added theorem CategoryTheory.Functor.postcomp_map_heq

deleted theorem CategoryTheory.Functor.precomp_map_hEq

added theorem CategoryTheory.Functor.precomp_map_heq