Commit 2024-05-25 10:04 b6711569

feat(CategoryTheory/Action): category of continuous actions (#13006) Introduces the category ContAction V G for any concrete category V with a forgetful functor to TopCat and monoid G. It is realized as a full subcategory of Action V G where the induced action is continuous. Also introduces the full subcategory DiscreteContAction V G where the underlying topological space is discrete.