OAI/SetTheory/PartitionPrinciple/Transfinite/GroundCompressionPrefixGraphs.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.compressionPrefixValue line 10
  2. theorem OAI.PartitionPilot.Forcing.compressionPrefixValue_old line 20
  3. theorem OAI.PartitionPilot.Forcing.compressionPrefixValue_stamp line 25
  4. theorem OAI.PartitionPilot.Forcing.compressionPrefixValue_limit line 36
  5. theorem OAI.PartitionPilot.Forcing.compressionPrefixValue_eq_prior_below line 48
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.compressionPrefixValue_mem line 61
  7. structure OAI.PartitionPilot.Forcing.GroundChronologyFields line 85
  8. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.graphFunction line 97
  9. def OAI.PartitionPilot.Forcing.GroundChronologyFields.value line 100
  10. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.value_entry line 103
  11. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.value_eq_of_entry line 107
  12. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.value_ground line 111
  13. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.value_mem_bound line 114
  14. def OAI.PartitionPilot.Forcing.GroundChronologyFields.codeFields line 118
  15. def OAI.PartitionPilot.Forcing.GroundChronologyFields.code line 121
  16. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.code_ground line 123
  17. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.code_eq_iff line 128
  18. def OAI.PartitionPilot.Forcing.compressionPrefixGraph line 141
  19. theorem OAI.PartitionPilot.Forcing.compressionPrefixGraph_entries line 146
  20. theorem OAI.PartitionPilot.Forcing.compressionPrefixGraph_exact line 169
  21. theorem OAI.PartitionPilot.Forcing.compressionPrefixGraph_function line 199
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.compressionPrefixGraph_mem line 226
  23. def OAI.PartitionPilot.Forcing.GroundChronologyFields.ofGraphs line 247
  24. theorem OAI.PartitionPilot.Forcing.GroundChronologyFields.ofGraphs_graph line 276