OAI/SetTheory/PartitionPrinciple/Definability/GroundRefinementPairClassGraphs.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finite_set_code line 16
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finite_mem line 31
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finite_range_mem line 38
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finite_function_graph_mem line 51
  5. def OAI.PartitionPilot.Forcing.familyCodeGraph line 74
  6. theorem OAI.PartitionPilot.Forcing.mem_familyCodeGraph line 78
  7. theorem OAI.PartitionPilot.Forcing.pair_mem_familyCodeGraph line 83
  8. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_isFunc line 96
  9. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_function line 108
  10. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_restrict line 113
  11. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_finite_ground line 132
  12. theorem OAI.PartitionPilot.Forcing.rank_finiteCodeRange_lt line 142
  13. theorem OAI.PartitionPilot.Forcing.familyCodeGraph_finite_rank_lt line 158
  14. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.graph line 176
  15. theorem OAI.PartitionPilot.Forcing.GroundDefinableFunction.mem_graph line 180
  16. theorem OAI.PartitionPilot.Forcing.GroundDefinableFunction.pair_mem_graph line 190
  17. theorem OAI.PartitionPilot.Forcing.GroundDefinableFunction.graph_function line 201
  18. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.graphPairFormula line 216
  19. theorem OAI.PartitionPilot.Forcing.GroundDefinableFunction.realize_graphPairFormula line 220
  20. theorem OAI.PartitionPilot.Forcing.GroundDefinableFunction.graph_mem line 240
  21. def OAI.PartitionPilot.Forcing.SetFormula.orbitCodeEntryFormula line 269
  22. def OAI.PartitionPilot.Forcing.SetFormula.orbitCodeEqualityFormula line 273
  23. def OAI.PartitionPilot.Forcing.SetFormula.orbitCodeFamilyPairFormula line 276
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orbitCodeEntry_meaning line 292
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orbitCodeEquality_meaning line 316
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orbitCodeFamilyPair_meaning line 326
  27. def OAI.PartitionPilot.Forcing.TransitiveGround.orbitCodeFamily line 354
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_orbitCodeFamily line 358
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orbitCodeFamily_function line 368
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orbitCodeFamily_mem line 381
  31. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.graphCodeFormula line 412
  32. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.definable_graph line 420
  33. def OAI.PartitionPilot.Forcing.Name.refinementClassGraph line 462
  34. theorem OAI.PartitionPilot.Forcing.Name.mem_refinementClassGraph line 468
  35. theorem OAI.PartitionPilot.Forcing.Name.pair_mem_refinementClassGraph line 480
  36. theorem OAI.PartitionPilot.Forcing.Name.refinementClassGraph_function line 495
  37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementClassGraph_mem line 519
  38. def OAI.PartitionPilot.Forcing.orderedPairNameGraph line 569
  39. theorem OAI.PartitionPilot.Forcing.mem_orderedPairNameGraph line 574
  40. def OAI.PartitionPilot.Forcing.SetFormula.orderedPairNameGraphEntryFormula line 589
  41. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_orderedPairNameGraphEntryFormula line 599
  42. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orderedPairNameGraph_mem line 635
  43. def OAI.PartitionPilot.Forcing.Name.refinementPairClassGraph line 669
  44. theorem OAI.PartitionPilot.Forcing.Name.pair_mem_refinementPairClassGraph line 675
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementPairClassGraph_mem line 699