Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-01 04:43 8195826f

View on Github →

refactor(category theory/cofiltered_systems): rename mittag_leffler.lean and move nonempty_sections_of_fintype_cofiltered_system into new file (#18433)

Create new file category_theory/cofiltered_system.lean.
Delete category_theory/mittag_leffler.lean and move its content there.
Move nonempty_sections_of_fintype_cofiltered_system and nonempty_sections_of_fintype_inverse_system there.
Some new lemmas.

Estimated changes

Renamed src/category_theory/mittag_leffler.lean to src/category_theory/cofiltered_system.lean

added theorem category_theory.functor.eval_section_injective_of_eventually_injective

added theorem category_theory.functor.eval_section_surjective_of_surjective

added theorem category_theory.functor.eventually_injective

modified theorem category_theory.functor.surjective_to_eventual_ranges

modified theorem category_theory.functor.thin_diagram_of_surjective

added theorem category_theory.functor.to_preimages_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

Modified src/combinatorics/hall/basic.lean

Modified src/combinatorics/simple_graph/ends/defs.lean

Modified src/combinatorics/simple_graph/finsubgraph.lean

Modified src/topology/category/Top/limits.lean

modified theorem Top.partial_sections.nonempty

deleted theorem nonempty_sections_of_fintype_cofiltered_system.init

deleted theorem nonempty_sections_of_fintype_cofiltered_system

deleted theorem nonempty_sections_of_fintype_inverse_system