OAI/SetTheory/PartitionPrinciple/Definability/DepthSlotCodes.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.natSuccessorGraph line 10
  2. def OAI.PartitionPilot.Forcing.natAddGraph line 13
  3. def OAI.PartitionPilot.Forcing.natMulGraph line 17
  4. theorem OAI.PartitionPilot.Forcing.pair_mem_natSuccessorGraph line 21
  5. theorem OAI.PartitionPilot.Forcing.pair_mem_natAddGraph line 28
  6. theorem OAI.PartitionPilot.Forcing.pair_mem_natMulGraph line 37
  7. theorem OAI.PartitionPilot.Forcing.natSuccessorGraph_isFunc line 46
  8. theorem OAI.PartitionPilot.Forcing.natAddGraph_isFunc line 49
  9. theorem OAI.PartitionPilot.Forcing.natMulGraph_isFunc line 53
  10. def OAI.PartitionPilot.Forcing.natAddSection line 57
  11. theorem OAI.PartitionPilot.Forcing.natAddSection_eq line 60
  12. theorem OAI.PartitionPilot.Forcing.natIterate_successor line 75
  13. theorem OAI.PartitionPilot.Forcing.natIterate_add line 81
  14. def OAI.PartitionPilot.Forcing.depthSlotIndex line 87
  15. theorem OAI.PartitionPilot.Forcing.depthSlotIndex_lt_iff line 89
  16. theorem OAI.PartitionPilot.Forcing.depthSlotIndex_eq_iff line 94
  17. theorem OAI.PartitionPilot.Forcing.depthSlotIndex_le_iff line 99
  18. def OAI.PartitionPilot.Forcing.depthSlotGraph line 104
  19. theorem OAI.PartitionPilot.Forcing.mem_depthSlotGraph line 111
  20. theorem OAI.PartitionPilot.Forcing.pair_mem_depthSlotGraph line 122
  21. theorem OAI.PartitionPilot.Forcing.depthSlotGraph_eq line 140
  22. theorem OAI.PartitionPilot.Forcing.depthSlotGraph_function line 158
  23. theorem OAI.PartitionPilot.Forcing.depthSlotGraph_injection line 163