OAI/SetTheory/PartitionPrinciple/Transfinite/GroundMainPrefixTopColumns.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeFamily line 17
  2. def OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeValues line 20
  3. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeFamily_ground line 23
  4. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeFamily_function line 28
  5. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeFamily_entry line 31
  6. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRange_stage_eq line 36
  7. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeFamily_stage_entry line 48
  8. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeValues_ground line 53
  9. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeValues_union line 56
  10. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeFamily_rank_le_code line 62
  11. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeValues_rank_le_code line 67
  12. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeightRange_rank_le_code line 70
  13. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.heightRangeValues_countable line 79
  14. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeightRange_countable line 86
  15. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_relationImage_eq line 109
  16. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.limitHeight_relationImage_countable line 117
  17. def OAI.PartitionPilot.Forcing.GroundMainPrefix.stageTopHeight line 125
  18. def OAI.PartitionPilot.Forcing.GroundMainPrefix.stageTopColumn line 129
  19. def OAI.PartitionPilot.Forcing.GroundMainPrefix.topHeightFamily line 134
  20. def OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnFamily line 136
  21. def OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnValues line 138
  22. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageTopHeight_entry line 140
  23. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.stageTopHeight_column line 144
  24. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topHeightFamily_ground line 155
  25. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnFamily_ground line 164
  26. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topHeightFamily_function line 175
  27. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnFamily_function line 178
  28. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topHeightFamily_entry line 181
  29. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnFamily_entry line 185
  30. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnValues_ground line 189
  31. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnValues_subset line 192
  32. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topHeightFamily_rank_le_code line 197
  33. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnFamily_rank_le_code line 202
  34. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnValues_rank_le_code line 212
  35. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.topColumnValues_countable line 215
  36. theorem OAI.PartitionPilot.Forcing.GroundMainPrefix.height_column_below_topColumn line 226