OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixLimitChronologyCore.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.related_birth_iff line 17
  2. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoint_birth_iff line 25
  3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.related_height_iff line 34
  4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoint_height_iff line 42
  5. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitValueGraph line 55
  6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitValueGraph_ground line 58
  7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitValueGraph_entry line 63
  8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitValueGraph_at line 84
  9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitValueGraph_rank_lt line 101
  10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPoint_old_birth_coverage line 111
  11. def OAI.PartitionPilot.Forcing.GroundMainPrefix.LimitBirthValue line 126
  12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirthValue_at line 130
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirthValue_total line 140
  14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirthValue_unique line 146
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirthValue_old_fiber line 153
  16. def OAI.PartitionPilot.Forcing.GroundMainPrefix.heightValueBound line 168
  17. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightValueBound_ground line 170
  18. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.height_value_mem_bound line 173
  19. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightValueBound_rank_le_code line 177
  20. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight line 180
  21. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_ground line 183
  22. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_entry line 186
  23. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_at line 193
  24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_function line 201
  25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_height line 217
  26. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_rank_lt line 223
  27. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirth line 231
  28. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirth_ground line 234
  29. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirth_entry line 237
  30. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirth_function line 242
  31. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirth_at line 251
  32. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitPointMap_birth_iff line 257
  33. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirth_old_fiber line 263
  34. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitBirth_rank_lt line 274
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_code line 282
  36. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeightRange line 291
  37. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeightRange_ground line 293
  38. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeightRange_mem line 296
  39. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeightRange_rank_lt line 308
  40. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limit_old_meet line 316
  41. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitTerminalFields line 332
  42. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitTerminalFields_ground line 336
  43. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitTerminalPoint line 340
  44. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitTerminalFields_rank_lt line 352
  45. def OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyFields line 362
  46. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyFields_graph line 366
  47. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyFields_terminal line 370
  48. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyFields_values line 374
  49. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyFields_source_entries line 380
  50. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyFields_graph_rank_lt line 389
  51. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyPoint line 401
  52. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitChronologyCore line 433