Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-27 21:53 937c692d

View on Github →

chore(category_theory): fix name of mono_app_of_mono (#16275) This PR fixes the names of a few lemmas like mono_app_of_mono.

Estimated changes

Modified src/category_theory/adjunction/evaluation.lean

deleted theorem category_theory.nat_trans.epi_iff_app_epi

added theorem category_theory.nat_trans.epi_iff_epi_app

deleted theorem category_theory.nat_trans.mono_iff_app_mono

added theorem category_theory.nat_trans.mono_iff_mono_app

Modified src/category_theory/functor/category.lean

deleted theorem category_theory.nat_trans.epi_app_of_epi

added theorem category_theory.nat_trans.epi_of_epi_app

deleted theorem category_theory.nat_trans.mono_app_of_mono

added theorem category_theory.nat_trans.mono_of_mono_app

Modified src/category_theory/sites/subsheaf.lean