Commit 2025-05-04 19:54 6733b4b5

View on Github →

feat(CategoryTheory/Action): functoriality for ContAction (#24562)

Estimated changes

Modified Mathlib/CategoryTheory/Action/Basic.lean

added def Action.resCongr

added def Action.resEquiv

added def CategoryTheory.Functor.Equivalence.mapAction

added def CategoryTheory.Functor.mapActionComp

added def CategoryTheory.Functor.mapActionCongr

Modified Mathlib/CategoryTheory/Action/Continuous.lean

added theorem Action.isContinuous_def

added def CategoryTheory.Equivalence.mapContAction

added def CategoryTheory.Functor.mapContAction

added def CategoryTheory.Functor.mapContActionComp

added def CategoryTheory.Functor.mapContActionCongr

added def ContAction.res

added def ContAction.resComp

added def ContAction.resCongr

added def ContAction.resEquiv