Commit 2024-11-23 13:41 a4de385a

View on Github →

feat(CategoryTheory): add some API for countable products and countable filtered colimits (#19192)

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Countable.lean

added theorem CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_aux

added theorem CategoryTheory.Limits.IsCofiltered.sequentialFunctor_map

added theorem CategoryTheory.Limits.IsFiltered.sequentialFunctor_final_aux

added theorem CategoryTheory.Limits.IsFiltered.sequentialFunctor_map

deleted theorem CategoryTheory.Limits.sequentialFunctor_initial_aux

deleted theorem CategoryTheory.Limits.sequentialFunctor_map

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean