OAI/SetTheory/PartitionPrinciple/Definability/GroundRationalCodes.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.gridStep line 13
  2. theorem OAI.PartitionPilot.Forcing.gridStep_pair line 18
  3. theorem OAI.PartitionPilot.Forcing.gridStep_eq_iff line 32
  4. def OAI.PartitionPilot.Forcing.liftedGridStep line 38
  5. theorem OAI.PartitionPilot.Forcing.gridIteration_pair line 41
  6. def OAI.PartitionPilot.Forcing.omegaGridEquiv line 50
  7. theorem OAI.PartitionPilot.Forcing.gridIteration_eq line 61
  8. def OAI.PartitionPilot.Forcing.positiveMagnitude line 76
  9. def OAI.PartitionPilot.Forcing.negativeMagnitude line 79
  10. def OAI.PartitionPilot.Forcing.fractionComparison line 85
  11. theorem OAI.PartitionPilot.Forcing.exists_mem_omega_code line 95
  12. theorem OAI.PartitionPilot.Forcing.positiveMagnitude_ofNat line 104
  13. theorem OAI.PartitionPilot.Forcing.positiveMagnitude_negSucc line 111
  14. theorem OAI.PartitionPilot.Forcing.negativeMagnitude_ofNat line 118
  15. theorem OAI.PartitionPilot.Forcing.negativeMagnitude_negSucc line 124
  16. theorem OAI.PartitionPilot.Forcing.fractionComparison_code line 134
  17. def OAI.PartitionPilot.Forcing.BoundedFormula.positiveMagnitudeFormula line 161
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.negativeMagnitudeFormula line 164
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_positiveMagnitudeFormula line 170
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_negativeMagnitudeFormula line 176
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.fractionComparisonFormula line 183
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_fractionComparisonFormula line 201
  23. def OAI.PartitionPilot.Forcing.GridStepCode line 223
  24. theorem OAI.PartitionPilot.Forcing.gridStepCode_nat line 227
  25. def OAI.PartitionPilot.Forcing.BoundedFormula.gridStepFormula line 244
  26. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_gridStepFormula line 250
  27. def OAI.PartitionPilot.Forcing.BoundedFormula.gridTransitionFormula line 255
  28. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_gridTransitionFormula line 260
  29. def OAI.PartitionPilot.Forcing.BoundedFormula.gridEntryFormula line 267
  30. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_gridEntryFormula line 271
  31. theorem OAI.PartitionPilot.Forcing.BoundedFormula.gridEntry_correct line 279
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.gridStep_graph_mem line 317
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.omega_grid_equiv_graph_mem line 341
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.omega_product_countable line 357
  35. def OAI.PartitionPilot.Forcing.BoundedFormula.fractionGraphFormula line 386
  36. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_fractionGraphFormula line 393
  37. theorem OAI.PartitionPilot.Forcing.BoundedFormula.fractionGraphFormula_iff line 403
  38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fractionCarrier_mem line 436
  39. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fractionComparisonGraph_mem line 448
  40. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fractionEquivGraph_mem line 475
  41. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fractionLtGraph_mem line 482
  42. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fractionCarrier_countable line 501
  43. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rationalCarrier_mem line 516
  44. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rationalLtGraph_mem line 527
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundRationals line 538