Commit 2025-01-29 09:37 5e04c482

View on Github →

feat(CategoryTheory): the subpresheaf of types generated by a section (#21174)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subpresheaf/OfSection.lean

added theorem CategoryTheory.Subpresheaf.mem_ofSection_obj

added def CategoryTheory.Subpresheaf.ofSection

added theorem CategoryTheory.Subpresheaf.ofSection_eq_range'

added theorem CategoryTheory.Subpresheaf.ofSection_eq_range

added theorem CategoryTheory.Subpresheaf.ofSection_image

added theorem CategoryTheory.Subpresheaf.ofSection_le_iff

added theorem CategoryTheory.Subpresheaf.range_eq_ofSection'

added theorem CategoryTheory.Subpresheaf.range_eq_ofSection