Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-03 06:58 6cb77a8e

View on Github →

feat(category_theory/mittag_leffler): Introduce the Mittag-Leffler condition (#17905)

depends on: #18013

Estimated changes

Created src/category_theory/mittag_leffler.lean

added def category_theory.functor.eventual_range

added theorem category_theory.functor.eventual_range_eq_iff

added theorem category_theory.functor.eventual_range_eq_range_precomp

added theorem category_theory.functor.eventual_range_maps_to

added theorem category_theory.functor.is_mittag_leffler.eq_image_eventual_range

added theorem category_theory.functor.is_mittag_leffler.subset_image_eventual_range

added theorem category_theory.functor.is_mittag_leffler.to_preimages

added def category_theory.functor.is_mittag_leffler

added theorem category_theory.functor.is_mittag_leffler_iff_eventual_range

added theorem category_theory.functor.is_mittag_leffler_iff_subset_range_comp

added theorem category_theory.functor.is_mittag_leffler_of_exists_finite_range

added theorem category_theory.functor.is_mittag_leffler_of_surjective

added theorem category_theory.functor.mem_eventual_range_iff

added theorem category_theory.functor.surjective_to_eventual_ranges

added theorem category_theory.functor.thin_diagram_of_surjective

added def category_theory.functor.to_eventual_ranges

added theorem category_theory.functor.to_eventual_ranges_nonempty

added def category_theory.functor.to_eventual_ranges_sections_equiv

added def category_theory.functor.to_preimages

Modified src/order/directed.lean

added theorem directed_on.is_bot_of_is_min

added theorem directed_on.is_top_of_is_max

added theorem directed_on_range