Commit 2025-02-18 21:48 d7c8ad59

View on Github →

feat(CategoryTheory/Subpresheaf): the order isomorphism Subpresheaf F ≃o Subobject F. (#21104)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subpresheaf/Subobject.lean

added theorem CategoryTheory.Subpresheaf.range_subobjectMk_ι

added theorem CategoryTheory.Subpresheaf.subobjectMk_range_arrow