Documentation Verification Report

Functors

📁 Source: Mathlib/Condensed/Functors.lean

Statistics

Metric	Count
Definitions `toCondensed`, `ulift`, `toCondensed`, `toCondensed`, `compHausToCondensed`, `compHausToCondensed'`, `profiniteToCondensed`, `stoneanToCondensed`	8
Theorems `instFaithfulCompHausCondensedSetCompHausToCondensed`, `instFaithfulCompHausCondensedTypeCompHausToCondensed'`, `instFaithfulCondensedTypeCondensedSetUlift`, `instFullCompHausCondensedSetCompHausToCondensed`, `instFullCompHausCondensedTypeCompHausToCondensed'`, `instFullCondensedTypeCondensedSetUlift`, `instPreservesFiniteCoproductsCompHausCondensedSetCompHausToCondensed`	7
Total	15

CompHaus

Definitions

Name	Category	Theorems
`toCondensed` 📖	CompOp	—

Condensed

Definitions

Name	Category	Theorems
`ulift` 📖	CompOp	2 math math: `instFaithfulCondensedTypeCondensedSetUlift`, `instFullCondensedTypeCondensedSetUlift`

Profinite

Definitions

Name	Category	Theorems
`toCondensed` 📖	CompOp	—

Stonean

Definitions

Name	Category	Theorems
`toCondensed` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`compHausToCondensed` 📖	CompOp	4 math math: `instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed`, `instFullCompHausCondensedSetCompHausToCondensed`, `instPreservesFiniteCoproductsCompHausCondensedSetCompHausToCondensed`, `instFaithfulCompHausCondensedSetCompHausToCondensed`
`compHausToCondensed'` 📖	CompOp	2 math math: `instFullCompHausCondensedTypeCompHausToCondensed'`, `instFaithfulCompHausCondensedTypeCompHausToCondensed'`
`profiniteToCondensed` 📖	CompOp	—
`stoneanToCondensed` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulCompHausCondensedSetCompHausToCondensed` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CompHaus` `CompHausLike.category` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `compHausToCondensed`	—	—
`instFaithfulCompHausCondensedTypeCompHausToCondensed'` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CompHaus` `CompHausLike.category` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `compHausToCondensed'`	—	—
`instFaithfulCondensedTypeCondensedSetUlift` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `CondensedSet` `Condensed.ulift`	—	`CategoryTheory.instFaithfulSheafSheafCompose` `CategoryTheory.uliftFunctor_faithful`
`instFullCompHausCondensedSetCompHausToCondensed` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CompHaus` `CompHausLike.category` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `compHausToCondensed`	—	—
`instFullCompHausCondensedTypeCompHausToCondensed'` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CompHaus` `CompHausLike.category` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `compHausToCondensed'`	—	—
`instFullCondensedTypeCondensedSetUlift` 📖	mathematical	—	`CategoryTheory.Functor.Full` `Condensed` `CategoryTheory.types` `instCategoryCondensed` `CondensedSet` `Condensed.ulift`	—	`CategoryTheory.instFullSheafSheafComposeOfFaithful` `CategoryTheory.uliftFunctor_full` `CategoryTheory.uliftFunctor_faithful`
`instPreservesFiniteCoproductsCompHausCondensedSetCompHausToCondensed` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteCoproducts` `CompHaus` `CompHausLike.category` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `compHausToCondensed`	—	—

---

← Back to Index