Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-05 23:47 7cc367b7

View on Github →

feat(category_theory/subobject): minor tweaks (#7466) A few minor tweaks to the subobject API that I wanted while working on homology.

Estimated changes

Modified src/category_theory/subobject/basic.lean

added theorem category_theory.subobject.of_le_mk_le_mk_of_comm

Modified src/category_theory/subobject/factor_thru.lean

deleted theorem category_theory.subobject.factor_thru_comp_of_le

added theorem category_theory.subobject.factor_thru_of_le

Modified src/category_theory/subobject/lattice.lean

deleted def category_theory.subobject.top_coe_iso_self

deleted theorem category_theory.subobject.underlying_iso_id_eq_top_coe_iso_self

added theorem category_theory.subobject.underlying_iso_top_hom