Mathlib Changelog
Changelog
About
Github
Commit
2021-04-22 14:56
1f65e42e
View on Github →
feat(category_theory/adjunction): reflective adjunction induces partial bijection (
#7286
)
Estimated changes
Modified
src/category_theory/adjunction/reflective.lean
added
def
category_theory.unit_comp_partial_bijective
added
def
category_theory.unit_comp_partial_bijective_aux
added
theorem
category_theory.unit_comp_partial_bijective_aux_symm_apply
added
theorem
category_theory.unit_comp_partial_bijective_natural
added
theorem
category_theory.unit_comp_partial_bijective_symm_apply
added
theorem
category_theory.unit_comp_partial_bijective_symm_natural