Commit 2023-05-15 10:06 ae53970a

View on Github →

feat: port CategoryTheory.CofilteredSystem (#3977)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/CofilteredSystem.lean

added theorem CategoryTheory.Functor.IsMittagLeffler.eq_image_eventualRange

added theorem CategoryTheory.Functor.IsMittagLeffler.subset_image_eventualRange

added theorem CategoryTheory.Functor.IsMittagLeffler.toPreimages

added def CategoryTheory.Functor.IsMittagLeffler

added theorem CategoryTheory.Functor.eval_section_injective_of_eventually_injective

added theorem CategoryTheory.Functor.eval_section_surjective_of_surjective

added def CategoryTheory.Functor.eventualRange

added theorem CategoryTheory.Functor.eventualRange_eq_iff

added theorem CategoryTheory.Functor.eventualRange_eq_range_precomp

added theorem CategoryTheory.Functor.eventualRange_mapsTo

added theorem CategoryTheory.Functor.eventually_injective

added theorem CategoryTheory.Functor.isMittagLeffler_iff_eventualRange

added theorem CategoryTheory.Functor.isMittagLeffler_iff_subset_range_comp

added theorem CategoryTheory.Functor.isMittagLeffler_of_exists_finite_range

added theorem CategoryTheory.Functor.isMittagLeffler_of_surjective

added theorem CategoryTheory.Functor.mem_eventualRange_iff

added theorem CategoryTheory.Functor.surjective_toEventualRanges

added theorem CategoryTheory.Functor.thin_diagram_of_surjective

added def CategoryTheory.Functor.toEventualRanges

added def CategoryTheory.Functor.toEventualRangesSectionsEquiv

added theorem CategoryTheory.Functor.toEventualRanges_nonempty

added def CategoryTheory.Functor.toPreimages

added theorem CategoryTheory.Functor.toPreimages_nonempty_of_surjective

added theorem nonempty_sections_of_finite_cofiltered_system.init

added theorem nonempty_sections_of_finite_cofiltered_system

added theorem nonempty_sections_of_finite_inverse_system