OAI/SetTheory/PartitionPrinciple/Geometry/GroundPreparationFamilyImages.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.leastSlotFormula line 11
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_leastSlotFormula line 15
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.leastSlotOwnerEntryFormula line 21
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_leastSlotOwnerEntryFormula line 28
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.leastSlotOwnerGraph_mem line 44
  6. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOwnerSlots line 78
  7. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSeedCarrier_ground line 106
  8. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerSlots_ground_function line 111
  9. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerSlots_monotone line 123
  10. theorem OAI.PartitionPilot.Forcing.pairedGraph_function_of_subset line 152
  11. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOwnerDepth line 173
  12. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOwnerLevelPairs line 180
  13. def OAI.PartitionPilot.Forcing.GroundCompressionCompletion.externalOwnerLevels line 184
  14. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerDepth_ground_function line 214
  15. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevelPairs_ground_function line 224
  16. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_ground_function line 235
  17. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_entry_iff line 247
  18. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_monotone line 276
  19. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_rank line 325
  20. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_equal_components line 345
  21. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_meet_lower line 360
  22. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_meet_old_or_lower line 393
  23. def OAI.PartitionPilot.Forcing.preparationFamilyImage line 417
  24. def OAI.PartitionPilot.Forcing.preparationFamilyFirst line 421
  25. def OAI.PartitionPilot.Forcing.preparationFamilySecond line 425
  26. theorem OAI.PartitionPilot.Forcing.preparationFamilyImage_function line 429
  27. theorem OAI.PartitionPilot.Forcing.preparationFamilyImages_function line 458
  28. theorem OAI.PartitionPilot.Forcing.preparationFamilyImages_entry line 467
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.preparationFamilyImages_mem line 521
  30. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalTileSlotPoints_support line 576
  31. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerSlots_supported line 584
  32. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_slot_support line 590
  33. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalOwnerLevels_slot_bound line 600
  34. theorem OAI.PartitionPilot.Forcing.GroundExternalGeometryInputs.externalSlotCopy_old_or_level_bound line 634