Commit 2024-02-24 11:39 558a4f94

View on Github →

feat: final functors with filtered codomain (#10892)

Estimated changes

Modified Mathlib/CategoryTheory/Filtered/Final.lean

added theorem CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful

added theorem CategoryTheory.Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful

added theorem CategoryTheory.IsCofiltered.of_exists_of_isCofiltered_of_fullyFaithful

added theorem CategoryTheory.IsCofilteredOrEmpty.of_exists_of_isCofiltered_of_fullyFaithful

added theorem CategoryTheory.IsFiltered.of_exists_of_isFiltered_of_fullyFaithful

added theorem CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful