Commit 2023-06-12 14:10 e7386704

View on Github →

feat: final functors preserve filteredness (#4973) Also generalize some facts about IsFiltered to IsFilteredOrEmpty.

Estimated changes

Modified Mathlib/CategoryTheory/Filtered.lean

added theorem CategoryTheory.IsCofilteredOrEmpty.of_equivalence

added theorem CategoryTheory.IsCofilteredOrEmpty.of_isLeftAdjoint

added theorem CategoryTheory.IsCofilteredOrEmpty.of_left_adjoint

added theorem CategoryTheory.IsFilteredOrEmpty.of_equivalence

added theorem CategoryTheory.IsFilteredOrEmpty.of_isRightAdjoint

added theorem CategoryTheory.IsFilteredOrEmpty.of_right_adjoint

added theorem CategoryTheory.isCofilteredOrEmpty_of_isFilteredOrEmpty_op

added theorem CategoryTheory.isCofiltered_of_isFiltered_op

added theorem CategoryTheory.isFilteredOrEmpty_of_isCofilteredOrEmpty_op

added theorem CategoryTheory.isFiltered_of_isCofiltered_op

Modified Mathlib/CategoryTheory/Limits/Final.lean

added theorem CategoryTheory.IsCofiltered.of_initial

added theorem CategoryTheory.IsCofilteredOrEmpty.of_initial

added theorem CategoryTheory.IsFiltered.of_final

added theorem CategoryTheory.IsFilteredOrEmpty.of_final