InheritedFromHom

📁 Source: Mathlib/CategoryTheory/ObjectProperty/InheritedFromHom.lean

Statistics

Metric	Count
Definitions InheritedFromSource, InheritedFromTarget	2
Theorems instIsomorphismsOfIsClosedUnderIsomorphisms, instMin, of_hom_of_source, of_le, op, instIsomorphismsOfIsClosedUnderIsomorphisms, instMin, of_hom_of_target, of_le, op, of_inheritedFromSource, of_inheritedFromTarget	12
Total	14

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
InheritedFromSource 📖	CompData	4 math math: InheritedFromSource.instIsomorphismsOfIsClosedUnderIsomorphisms, InheritedFromTarget.op, InheritedFromSource.instMin, InheritedFromSource.of_le
InheritedFromTarget 📖	CompData	4 math math: InheritedFromTarget.instMin, InheritedFromTarget.of_le, InheritedFromTarget.instIsomorphismsOfIsClosedUnderIsomorphisms, InheritedFromSource.op

CategoryTheory.ObjectProperty.InheritedFromSource

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsomorphismsOfIsClosedUnderIsomorphisms 📖	mathematical	—	CategoryTheory.ObjectProperty.InheritedFromSource CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.ObjectProperty.prop_of_iso
instMin 📖	mathematical	—	CategoryTheory.ObjectProperty.InheritedFromSource CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice Prop.instCompleteLattice	—	of_hom_of_source
of_hom_of_source 📖	—	—	—	—	—
of_le 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.ObjectProperty.InheritedFromSource	—	of_hom_of_source
op 📖	mathematical	—	CategoryTheory.ObjectProperty.InheritedFromTarget Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.op CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.op	—	of_hom_of_source

CategoryTheory.ObjectProperty.InheritedFromTarget

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsomorphismsOfIsClosedUnderIsomorphisms 📖	mathematical	—	CategoryTheory.ObjectProperty.InheritedFromTarget CategoryTheory.MorphismProperty.isomorphisms	—	CategoryTheory.ObjectProperty.prop_of_iso
instMin 📖	mathematical	—	CategoryTheory.ObjectProperty.InheritedFromTarget CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice Prop.instCompleteLattice	—	of_hom_of_target
of_hom_of_target 📖	—	—	—	—	—
of_le 📖	mathematical	CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct Preorder.toLE PartialOrder.toPreorder CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	CategoryTheory.ObjectProperty.InheritedFromTarget	—	of_hom_of_target
op 📖	mathematical	—	CategoryTheory.ObjectProperty.InheritedFromSource Opposite CategoryTheory.Category.opposite CategoryTheory.ObjectProperty.op CategoryTheory.Category.toCategoryStruct CategoryTheory.MorphismProperty.op	—	of_hom_of_target

CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_inheritedFromSource 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms	—	CategoryTheory.ObjectProperty.InheritedFromSource.of_hom_of_source CategoryTheory.MorphismProperty.of_isIso CategoryTheory.Iso.isIso_hom
of_inheritedFromTarget 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms	—	CategoryTheory.ObjectProperty.InheritedFromTarget.of_hom_of_target CategoryTheory.MorphismProperty.of_isIso CategoryTheory.Iso.isIso_inv

---

← Back to Index