Documentation Verification Report

SiteLocal

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

Statistics

Metric	Count
Definitions `IsLocal`	1
Theorems `component`, `inf`, `mk_of_zeroHypercover`, `of_le`, `of_presieve`, `toIsClosedUnderIsomorphisms`, `top`, `iff_of_presieve`, `iff_of_zeroHypercover`, `of_zeroHypercover`	10
Total	11

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsLocal` 📖	CompData	4 math math: `IsLocal.inf`, `IsLocal.mk_of_zeroHypercover`, `IsLocal.top`, `IsLocal.of_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_of_presieve` 📖	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings`	—	—	`IsLocal.component` `IsLocal.of_presieve`
`iff_of_zeroHypercover` 📖	mathematical	—	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover`	—	`IsLocal.component` `CategoryTheory.Precoverage.ZeroHypercover.mem₀` `of_zeroHypercover`
`of_zeroHypercover` 📖	—	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover`	—	—	`IsLocal.of_presieve` `CategoryTheory.Precoverage.ZeroHypercover.mem₀`

CategoryTheory.ObjectProperty.IsLocal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`component` 📖	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings`	—	—	—
`inf` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsLocal` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder`	—	`CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsMin` `toIsClosedUnderIsomorphisms` `component` `of_presieve`
`mk_of_zeroHypercover` 📖	mathematical	`CategoryTheory.PreZeroHypercover.X` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover`	`CategoryTheory.ObjectProperty.IsLocal`	—	`CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover`
`of_le` 📖	mathematical	`CategoryTheory.Precoverage` `Preorder.toLE` `PartialOrder.toPreorder` `CategoryTheory.Precoverage.instPartialOrder`	`CategoryTheory.ObjectProperty.IsLocal`	—	`toIsClosedUnderIsomorphisms` `component` `of_presieve`
`of_presieve` 📖	—	`CategoryTheory.Presieve` `Set` `Set.instMembership` `CategoryTheory.Precoverage.coverings`	—	—	—
`toIsClosedUnderIsomorphisms` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms`	—	—
`top` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsLocal` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsTop`

---

← Back to Index