OAI/Algebra/AuslanderReiten/Cones/TwoConeExtensionDiagrams.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.TwoCone.baseStepInclusion_mk line 14
2. def OAI.ArExplicit.TwoCone.middleStepInclusion line 17
3. def OAI.ArExplicit.TwoCone.singletonCoverLift line 21
4. theorem OAI.ArExplicit.TwoCone.singletonCoverLift_boundary line 24
5. theorem OAI.ArExplicit.TwoCone.singletonCoverLift_projection line 38
6. def OAI.ArExplicit.TwoCone.topCoverLift line 45
7. theorem OAI.ArExplicit.TwoCone.topCoverLift_boundary line 50
8. theorem OAI.ArExplicit.TwoCone.topCoverLift_projection line 64