OAI/SetTheory/PartitionPrinciple/Geometry/GroundMainFinalStructuralCompression.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.insertionUsedNodes line 13
2. theorem OAI.PartitionPilot.Forcing.mem_insertionUsedNodes line 18
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.insertionUsedNodes_mem_small line 36
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction_insertion_union line 87
5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.generated_insertion line 141
6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.decoded_generated_insertion line 174
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.generated_insertion_exceptions line 211
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_insertion_exceptions line 271
9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_compatible_insertion_unions line 445
10. theorem OAI.PartitionPilot.Forcing.PosetAction.compressed_name_support line 717
11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.FinalSupportFulfillment.structural_compression line 743