OAI/SetTheory/PartitionPrinciple/Forcing/GroundRefinementAssignmentActionFamilies.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementIndexActionFormula line 16
2. def OAI.PartitionPilot.Forcing.SetFormula.refinementIndexActionEntryFormula line 124
3. def OAI.PartitionPilot.Forcing.SetFormula.refinementIndexActionSetFormula line 129
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementIndexActionEntryFormula line 153
5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementIndexActionSetFormula line 201
6. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionGraph line 233
7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_stageOneAssignmentActionGraph line 238
8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneTermAction_function line 253
9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneTermAction_injection line 268
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionGraph_function line 291
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionGraph_mem line 300
12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionGraph_entry line 313
13. def OAI.PartitionPilot.Forcing.SetFormula.refinementIndexActionFamilyEntryFormula line 354
14. def OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionFamily line 367
15. def OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexFullActionGraph line 370
16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_niceRefinementIndexActionFamily line 376
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionFamily_function line 381
18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_niceRefinementIndexFullActionGraph line 390
19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexActionFamily_mem line 417
20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexFullActionGraph_mem line 473
21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexFullActionGraph_function line 480
22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.niceRefinementIndexFullActionGraph_entry line 498
23. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionGraph line 529
24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_refinementAssignmentActionGraph line 534
25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionGraph_zero line 545
26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionGraph_function line 562
27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionGraph_mem line 571
28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionGraph_entry line 584
29. def OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionFamily line 631
30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_stageOneAssignmentActionFamily line 634
31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionFamily_function line 639
32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionFamily_mem line 653
33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.stageOneAssignmentActionFamily_mem_of_inputs line 665
34. def OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionFamily line 699
35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_refinementAssignmentActionFamily line 702
36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionFamily_function line 707
37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionFamily_zero line 716
38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionFamily_mem line 725
39. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementAssignmentActionFamily_mem_of_inputs line 737