OAI/CategoryTheory/Thomason/Gray/
1689 declarations, 0 contain sorry, 0 declared as axioms; 31 files
Files
- ConstructedRightGray.lean 50 declarations
- CylinderAssembly.lean 59 declarations
- DirectedGlobeFaces.lean 82 declarations
- DirectedGlobeUniversal.lean 93 declarations
- FixedPathCylinders.lean 9 declarations
- GlobePastingDensity.lean 94 declarations
- GrayChainGlobeRestriction.lean 56 declarations
- GrayFinitePosetUnits.lean 12 declarations
- GrayMappingEndpointEvaluation.lean 66 declarations
- GrayMappingInterchangeEvaluation.lean 75 declarations
- GraySimplexProjection.lean 10 declarations
- GraySingularPathComparison.lean 10 declarations
- GridGlobeCylinderComparison.lean 85 declarations
- OrderedAtomGrouping.lean 43 declarations
- PastingGlobeChains.lean 81 declarations
- PastingGlobeCylinderAtoms.lean 43 declarations
- PastingGlobeCylinderPath.lean 55 declarations
- PastingGlobeCylinderRetractions.lean 72 declarations
- PosetPrismEndpoints.lean 71 declarations
- PrismSimplexNaturality.lean 75 declarations
- RightCylinderPrism.lean 85 declarations
- SimplexCylinderGeneration.lean 53 declarations
- SimplicialHomotopyWhiskering.lean 8 declarations
- SingularCylinderEquivalence.lean 24 declarations
- StrictAbelianization.lean 75 declarations
- SubdivisionPrismNaturality.lean 10 declarations
- TopologicalConePrism.lean 66 declarations
- TopologicalIntervalCylinder.lean 58 declarations
- TripleGlobeAtoms.lean 73 declarations
- TripleGlobeCylinderSource.lean 37 declarations
- TripleGlobeRetractions.lean 59 declarations