OAI/SetTheory/PartitionPrinciple/Geometry/RepresentativeIndexSteps.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.assignmentIndices line 9
  2. def OAI.PartitionPilot.Forcing.assignmentOnIndices line 12
  3. theorem OAI.PartitionPilot.Forcing.mem_assignmentIndices line 15
  4. theorem OAI.PartitionPilot.Forcing.mem_assignmentOnIndices line 30
  5. theorem OAI.PartitionPilot.Forcing.assignmentOnIndices_entry line 34
  6. theorem OAI.PartitionPilot.Forcing.assignmentIndices_on line 39
  7. theorem OAI.PartitionPilot.Forcing.assignmentOnIndices_own line 52
  8. theorem OAI.PartitionPilot.Forcing.assignment_subset_iff_indices_subset line 63
  9. def OAI.PartitionPilot.Forcing.AssignmentQueryWithin line 79
  10. def OAI.PartitionPilot.Forcing.assignmentQueriesWithin line 82
  11. def OAI.PartitionPilot.Forcing.representativeIndexAdditions line 85
  12. def OAI.PartitionPilot.Forcing.representativeIndexStep line 90
  13. theorem OAI.PartitionPilot.Forcing.mem_assignmentQueriesWithin line 93
  14. theorem OAI.PartitionPilot.Forcing.mem_representativeIndexAdditions line 97
  15. theorem OAI.PartitionPilot.Forcing.representativeIndexStep_contains line 104
  16. theorem OAI.PartitionPilot.Forcing.representativeIndexStep_subset line 108
  17. theorem OAI.PartitionPilot.Forcing.representativeIndexStep_covers line 114
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentIndices_mem line 137
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentOnIndices_mem line 143
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentIndices_small line 151
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentOnIndices_small line 160
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.assignmentOnIndices_candidate line 168
  23. theorem OAI.PartitionPilot.Forcing.stageOneRawTests_transfer line 186
  24. theorem OAI.PartitionPilot.Forcing.stageOneRawTests_congr line 196
  25. theorem OAI.PartitionPilot.Forcing.stageOneRawTests_cut_iff line 205
  26. theorem OAI.PartitionPilot.Forcing.stageTwoConditionCode_pair_iff line 214
  27. theorem OAI.PartitionPilot.Forcing.stageTwoConditionCode_cut_iff line 225
  28. theorem OAI.PartitionPilot.Forcing.packedSuccessorConditionCode_cut_iff line 234
  29. def OAI.PartitionPilot.Forcing.AssignmentIndexAgreement line 251
  30. theorem OAI.PartitionPilot.Forcing.stageOneRawTests_binary_union line 256
  31. def OAI.PartitionPilot.Forcing.stageOneRawCrossCollisions line 280
  32. theorem OAI.PartitionPilot.Forcing.stageOneRawTests_mixed_union line 287
  33. theorem OAI.PartitionPilot.Forcing.assignment_representative_agreement line 309
  34. def OAI.PartitionPilot.Forcing.TransitiveGround.classSelectionDefinition line 353
  35. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_assignmentClassGraph line 371
  36. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_assignmentOnIndices line 377
  37. def OAI.PartitionPilot.Forcing.TransitiveGround.storedAssignmentClassGraph line 386
  38. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_storedAssignmentClassGraph line 391
  39. def OAI.PartitionPilot.Forcing.TransitiveGround.storedPreparationRequests line 420
  40. def OAI.PartitionPilot.Forcing.TransitiveGround.relationImageDefinition line 426
  41. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_storedPreparationRequests line 441
  42. theorem OAI.PartitionPilot.Forcing.TransitiveGround.storedPreparationRequests_mem line 454
  43. theorem OAI.PartitionPilot.Forcing.TransitiveGround.storedPreparationRequests_typed line 460