OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixFieldFamilies.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.indices_rank_le_code line 15
  2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageGraph_rank_le_code line 20
  3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.transitionGraph_rank_le_code line 25
  4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.key_rank_lt_code line 30
  5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.linkedCode_rank_lt_code line 34
  6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.mapCode_rank_lt_code line 38
  7. def OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldFamily line 43
  8. def OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierFamily line 46
  9. def OAI.PartitionPilot.Forcing.GroundMainPrefix.actorFamily line 48
  10. def OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapFamily line 50
  11. def OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapFamily line 53
  12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldFamily_ground line 56
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierFamily_ground line 66
  14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorFamily_ground line 68
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.mapFamilies_ground line 70
  16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapFamily_ground line 78
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapFamily_ground line 80
  18. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldFamily_function line 82
  19. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierFamily_function line 85
  20. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorFamily_function line 88
  21. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapFamily_function line 91
  22. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapFamily_function line 98
  23. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageFieldFamily_entry line 105
  24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.carrierFamily_entry line 109
  25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorFamily_entry line 113
  26. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.pointMapFamily_entry line 117
  27. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.actorMapFamily_entry line 123