ReflectsIso

📁 Source: Mathlib/CategoryTheory/ConcreteCategory/ReflectsIso.lean

Statistics

Metric	Count
Definitions	0
Theorems instReflectsIsomorphismsForgetTypeHom, reflectsIsomorphisms_forget₂	2
Total	2

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instReflectsIsomorphismsForgetTypeHom 📖	mathematical	—	Functor.ReflectsIsomorphisms types forget Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Types.instFunLike Types.instConcreteCategory	—	—
reflectsIsomorphisms_forget₂ 📖	mathematical	—	Functor.ReflectsIsomorphisms forget₂	—	isIso_of_reflects_iso HasForget₂.forget_comp Functor.map_isIso

---

← Back to Index