OAI/SetTheory/PartitionPrinciple/Transfinite/GroundInitialPreservedMainPrefix.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixGraphBodyFormula line 14
2. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixGraphFormula line 22
3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixGraphBodyFormula line 37
4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixGraphFormula line 64
5. def OAI.PartitionPilot.Forcing.SetFormula.mainPrefixFormula line 89
6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_mainPrefixFormula line 100
7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.code_eq_mainPrefixCode line 154
8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.code_valid line 156
9. def OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefixCandidates line 164
10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_mainPrefixCandidates line 167
11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mainPrefixCandidates_mem line 171
12. def OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validMainPrefixes line 200
13. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.validMainPrefixes_ground line 203
14. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.mem_validMainPrefixes line 214
15. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.prefix_mem_validMainPrefixes line 219
16. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.finite_prefix_mem_validMainPrefixes line 228
17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_initialMainPrefixCandidate line 248
18. theorem OAI.PartitionPilot.Forcing.MainPrefixCode.exists_decodedPrefix line 307
19. theorem OAI.PartitionPilot.Forcing.GroundMainCandidateLevel.exists_prefix_of_mem line 319
20. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.exists_rankedAppendTaskBearing line 344
21. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.fieldUnions_rank_le_codeRange line 415
22. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.unionCode_rank_lt_of_codeRange line 440
23. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.unionCode_rank_lt_small line 460
24. theorem OAI.PartitionPilot.Forcing.MainPrefixGraphFamily.unionCode_mem_validMainPrefixes line 465
25. def OAI.PartitionPilot.Forcing.SetFormula.preservedMainPrefixFormula line 479
26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_preservedMainPrefixFormula line 492
27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundInitialPreservedMainPrefix line 547