Documentation Verification Report

MulticoequalizerDiagram

📁 Source: Mathlib/Order/CompleteLattice/MulticoequalizerDiagram.lean

Statistics

Metric	Count
Definitions `MulticoequalizerDiagram`, `multicofork`, `multispanIndex`, `BicartSq`, `MulticoequalizerDiagram`	5
Theorems `eq_inf`, `iSup_eq`, `min_eq`, `multicofork_pt`, `multispanIndex_fst`, `multispanIndex_left`, `multispanIndex_right`, `multispanIndex_snd`, `commSq`, `inf_eq`, `le₁₂`, `le₁₃`, `le₂₄`, `le₃₄`, `max_eq`, `min_eq`, `multicoequalizerDiagram`, `sup_eq`	18
Total	23

CompleteLattice

Definitions

Name	Category	Theorems
`MulticoequalizerDiagram` 📖	CompData	1 math math: `Lattice.BicartSq.multicoequalizerDiagram`

CompleteLattice.MulticoequalizerDiagram

Definitions

Name	Category	Theorems
`multicofork` 📖	CompOp	1 math math: `multicofork_pt`
`multispanIndex` 📖	CompOp	19 math math: `SSet.horn₃₁.desc.multicofork_π_two`, `SSet.horn₃₂.desc.multicofork_π_one`, `SSet.horn₃₁.desc.multicofork_pt`, `multispanIndex_right`, `multispanIndex_fst`, `SSet.horn₃₁.desc.multicofork_π_two_assoc`, `SSet.horn₃₁.desc.multicofork_π_zero_assoc`, `multispanIndex_left`, `SSet.horn₃₂.desc.multicofork_π_zero_assoc`, `multispanIndex_snd`, `SSet.horn₃₁.desc.multicofork_π_three_assoc`, `SSet.horn₃₁.desc.multicofork_π_zero`, `SSet.horn₃₂.desc.multicofork_π_three`, `multicofork_pt`, `SSet.horn₃₂.desc.multicofork_pt`, `SSet.horn₃₂.desc.multicofork_π_zero`, `SSet.horn₃₂.desc.multicofork_π_three_assoc`, `SSet.horn₃₂.desc.multicofork_π_one_assoc`, `SSet.horn₃₁.desc.multicofork_π_three`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_inf` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	—
`iSup_eq` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`iSup` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup`	—	—
`min_eq` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice`	—	`eq_inf`
`multicofork_pt` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Limits.WalkingMultispan` `CategoryTheory.Limits.MultispanShape.prod` `CategoryTheory.Limits.WalkingMultispan.instSmallCategory` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `CategoryTheory.Limits.MultispanIndex.multispan` `multispanIndex` `multicofork`	—	—
`multispanIndex_fst` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`CategoryTheory.Limits.MultispanIndex.fst` `CategoryTheory.Limits.MultispanShape.prod` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `multispanIndex` `CategoryTheory.homOfLE` `CategoryTheory.Limits.MultispanShape.fst`	—	—
`multispanIndex_left` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`CategoryTheory.Limits.MultispanIndex.left` `CategoryTheory.Limits.MultispanShape.prod` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `multispanIndex`	—	—
`multispanIndex_right` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`CategoryTheory.Limits.MultispanIndex.right` `CategoryTheory.Limits.MultispanShape.prod` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `multispanIndex`	—	—
`multispanIndex_snd` 📖	mathematical	`CompleteLattice.MulticoequalizerDiagram`	`CategoryTheory.Limits.MultispanIndex.snd` `CategoryTheory.Limits.MultispanShape.prod` `Preorder.smallCategory` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `CompleteLattice.toCompleteSemilatticeInf` `multispanIndex` `CategoryTheory.homOfLE` `CategoryTheory.Limits.MultispanShape.snd`	—	—

Lattice

Definitions

Name	Category	Theorems
`BicartSq` 📖	CompData	—

Lattice.BicartSq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commSq` 📖	mathematical	`Lattice.BicartSq`	`CategoryTheory.CommSq` `Preorder.smallCategory` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `CategoryTheory.homOfLE` `le₁₂` `le₁₃` `le₂₄` `le₃₄`	—	`le₁₂` `le₁₃` `le₂₄` `le₃₄`
`inf_eq` 📖	mathematical	`Lattice.BicartSq`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	—
`le₁₂` 📖	mathematical	`Lattice.BicartSq`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`le₁₃` 📖	mathematical	`Lattice.BicartSq`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`le₂₄` 📖	mathematical	`Lattice.BicartSq`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`le₃₄` 📖	mathematical	`Lattice.BicartSq`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—
`max_eq` 📖	mathematical	`Lattice.BicartSq`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	`sup_eq`
`min_eq` 📖	mathematical	`Lattice.BicartSq`	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf`	—	`inf_eq`
`multicoequalizerDiagram` 📖	mathematical	`Lattice.BicartSq` `CompleteLattice.toLattice`	`CompleteLattice.MulticoequalizerDiagram`	—	`sup_eq` `sup_comm` `sup_eq_iSup`
`sup_eq` 📖	mathematical	`Lattice.BicartSq`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup`	—	—

SSet.Subcomplex

Definitions

Name	Category	Theorems
`MulticoequalizerDiagram` 📖	MathDef	1 math math: `SSet.horn.multicoequalizerDiagram`

---

← Back to Index