UnivLE

📁 Source: Mathlib/CategoryTheory/UnivLE.lean

Statistics

Metric	Count
Definitions witness	1
Theorems ofUnivLE, ofEssSurj, UnivLE_iff_essSurj, instFaithfulWitness, instFullWitness, instIsEquivalenceUliftFunctorOfUnivLE	6
Total	7

EssSurj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofUnivLE 📖	mathematical	—	CategoryTheory.Functor.EssSurj CategoryTheory.types CategoryTheory.uliftFunctor	—	UnivLE.small

UnivLE

Definitions

Name	Category	Theorems
witness 📖	CompOp	2 math math: instFaithfulWitness, instFullWitness

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofEssSurj 📖	mathematical	—	UnivLE	—	CategoryTheory.Functor.EssSurj.mem_essImage

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
UnivLE_iff_essSurj 📖	mathematical	—	UnivLE CategoryTheory.Functor.EssSurj CategoryTheory.types CategoryTheory.uliftFunctor	—	EssSurj.ofUnivLE UnivLE.ofEssSurj
instFaithfulWitness 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.types UnivLE.witness	—	instIsEquivalenceUliftFunctorOfUnivLE CategoryTheory.Functor.Faithful.comp CategoryTheory.uliftFunctor_faithful CategoryTheory.Functor.IsEquivalence.faithful CategoryTheory.Functor.isEquivalence_inv
instFullWitness 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.types UnivLE.witness	—	instIsEquivalenceUliftFunctorOfUnivLE CategoryTheory.Functor.Full.comp CategoryTheory.uliftFunctor_full CategoryTheory.Functor.IsEquivalence.full CategoryTheory.Functor.isEquivalence_inv
instIsEquivalenceUliftFunctorOfUnivLE 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence CategoryTheory.types CategoryTheory.uliftFunctor	—	CategoryTheory.uliftFunctor_faithful CategoryTheory.uliftFunctor_full EssSurj.ofUnivLE

---

← Back to Index