OAI/SetTheory/PartitionPrinciple/Geometry/GroundCompressionHeightSteps.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.lexHeightOrder line 13
  2. theorem OAI.PartitionPilot.Forcing.mem_lexHeightOrder line 19
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_lexHeightOrder line 31
  4. theorem OAI.PartitionPilot.Forcing.lexHeightOrder_code line 44
  5. def OAI.PartitionPilot.Forcing.StrictLexHeightCode.value line 87
  6. theorem OAI.PartitionPilot.Forcing.StrictLexHeightCode.value_entry line 93
  7. theorem OAI.PartitionPilot.Forcing.StrictLexHeightCode.value_eq_of_entry line 98
  8. theorem OAI.PartitionPilot.Forcing.StrictLexHeightCode.value_pair_iff line 103
  9. def OAI.PartitionPilot.Forcing.StrictLexHeightCode.toStrictHeight line 108
  10. theorem OAI.PartitionPilot.Forcing.StrictLexHeightCode.toStrictHeight_value_entry line 126
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.lexHeightEntryFormula line 137
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_lexHeightEntryFormula line 143
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.lexHeightOrder_mem line 158
  14. abbrev OAI.PartitionPilot.Forcing.BatchHeightEndpointCode.column line 192
  15. abbrev OAI.PartitionPilot.Forcing.BatchHeightEndpointCode.low line 194
  16. abbrev OAI.PartitionPilot.Forcing.BatchHeightEndpointCode.high line 196
  17. theorem OAI.PartitionPilot.Forcing.BatchHeightEndpointCode.column_entry line 199
  18. theorem OAI.PartitionPilot.Forcing.BatchHeightEndpointCode.low_entry line 201
  19. theorem OAI.PartitionPilot.Forcing.BatchHeightEndpointCode.high_entry line 203
  20. def OAI.PartitionPilot.Forcing.batchFreshHeightGraph line 208
  21. def OAI.PartitionPilot.Forcing.batchHeightGraph line 212
  22. theorem OAI.PartitionPilot.Forcing.batchHeightGraph_old_entry line 216
  23. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.batch_component_function line 233
  24. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.batch_fresh_function line 239
  25. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.batch_height_function line 250
  26. def OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.componentValue line 255
  27. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.componentValue_entry line 266
  28. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.componentValue_spec line 273
  29. def OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.componentStrictHeight line 283
  30. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.component_lower line 298
  31. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.component_upper line 315
  32. def OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.extendedHeight line 332
  33. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.encoded_height_entry line 340
  34. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.batchHeightGraph_strictLex line 353
  35. theorem OAI.PartitionPilot.Forcing.TemplateHeightFamilyInputs.batchHeightGraph_bound_preserved line 373
  36. theorem OAI.PartitionPilot.Forcing.FunctionGraphOn.constant_value line 411
  37. theorem OAI.PartitionPilot.Forcing.StrictLexHeightCode.strict_entry line 416
  38. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.constantTemplateHeights line 431
  39. def OAI.PartitionPilot.Forcing.fixedTopHeightGraph line 466
  40. theorem OAI.PartitionPilot.Forcing.pair_mem_fixedTopHeightGraph line 469
  41. theorem OAI.PartitionPilot.Forcing.fixedTopHeightGraph_old_iff line 474
  42. theorem OAI.PartitionPilot.Forcing.fixedTopHeightGraph_top_iff line 480
  43. theorem OAI.PartitionPilot.Forcing.fixedTopHeightGraph_function line 488
  44. theorem OAI.PartitionPilot.Forcing.fixedTopHeightGraph_strict line 507
  45. theorem OAI.PartitionPilot.Forcing.fixedTopHeightGraph_range line 529
  46. theorem OAI.PartitionPilot.Forcing.fixedTopHeightGraph_old_lt_top line 547
  47. theorem OAI.PartitionPilot.Forcing.fixedTopHeightGraph_bound line 556
  48. theorem OAI.PartitionPilot.Forcing.batchHeightGraph_columns line 570
  49. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchFreshHeightGraph_mem line 597
  50. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchHeightGraph_mem line 612
  51. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_batchHeight line 627
  52. theorem OAI.PartitionPilot.Forcing.TransitiveGround.fixedTopHeightGraph_mem line 705
  53. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_fixedTopHeight line 712
  54. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_batchHeight_of_countable_ranges line 778
  55. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_height_step line 832