OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainDiagramAppend.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.reindex line 18
2. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.CoversOldBirths.reindex line 24
3. structure OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone line 42
4. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.coneOfLast line 47
5. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone.appendStage line 58
6. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone.appendTransition line 62
7. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone.appendTransition_self line 74
8. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone.appendTransition_comp line 81
9. def OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone.append line 103
10. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone.append_reindex line 110
11. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.Cone.append_coverage line 112
12. theorem OAI.PartitionPilot.Forcing.GroundChronologicalMainDiagram.coneOfLast_coverage line 127