OAI/CategoryTheory/Thomason/Transfer/
458 declarations, 0 contain sorry, 0 declared as axioms; 21 files
Files
- FiniteCosieveAttachmentComparison.lean 4 declarations
- FiniteCosieveAttachmentCover.lean 5 declarations
- FiniteEmptyAttachmentFibers.lean 45 declarations
- FiniteStreetSievePushouts.lean 25 declarations
- FiveInputMainTheorem.lean 1 declarations
- GridGlobeCylinderPushout.lean 8 declarations
- HornAttachmentWeakEquivalences.lean 24 declarations
- HornRealizationGluing.lean 7 declarations
- KanQuillenLiftingReduction.lean 4 declarations
- Main.lean 14 declarations
- NonsingularFaceGluing.lean 21 declarations
- PastingGlobeCylinderPushout.lean 32 declarations
- SemanticMainTheorem.lean 4 declarations
- SimplicialRangeGluing.lean 47 declarations
- StreetLocalizationFromModel.lean 81 declarations
- StrictPushoutGeneration.lean 16 declarations
- ThomasonLeftProperness.lean 8 declarations
- ThomasonQuillenBridge.lean 56 declarations
- ThomasonSmallObject.lean 28 declarations
- TripleGlobeCylinderPushout.lean 15 declarations
- WeakFactorizationRecognition.lean 13 declarations