OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalTileSlotSupports.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.transportedTileCoordinates line 11
  2. theorem OAI.PartitionPilot.Forcing.pair_mem_transportedTileCoordinates line 18
  3. theorem OAI.PartitionPilot.Forcing.transportedTileCoordinates_partial line 33
  4. def OAI.PartitionPilot.Forcing.externalOwnerHeightGraph line 58
  5. theorem OAI.PartitionPilot.Forcing.pair_mem_externalOwnerHeightGraph line 64
  6. theorem OAI.PartitionPilot.Forcing.externalOwnerHeightGraph_old line 80
  7. theorem OAI.PartitionPilot.Forcing.externalOwnerHeightGraph_function line 87
  8. def OAI.PartitionPilot.Forcing.BoundedFormula.transportedTileCoordinateFormula line 138
  9. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_transportedTileCoordinateFormula line 148
  10. def OAI.PartitionPilot.Forcing.BoundedFormula.ownerHeightFreshFormula line 162
  11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ownerHeightFreshFormula line 172
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.transportedTileCoordinates_mem line 194
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalOwnerHeightGraph_mem line 217
  14. theorem OAI.PartitionPilot.Forcing.externalOwnerHeightGraph_range_subset line 248
  15. theorem OAI.PartitionPilot.Forcing.externalOwnerHeightGraph_below_cap line 261
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalOwnerHeightGraph_range_small line 283
  17. def OAI.PartitionPilot.Forcing.externalTileSlotSupports line 319
  18. theorem OAI.PartitionPilot.Forcing.pair_mem_externalTileSlotSupports line 327
  19. def OAI.PartitionPilot.Forcing.BoundedFormula.slotImageMembershipFormula line 345
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_slotImageMembershipFormula line 350
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.externalTileSlotSupportFormula line 364
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalTileSlotSupportFormula line 373
  23. theorem OAI.PartitionPilot.Forcing.externalOwnerHeightGraph_fresh line 393
  24. theorem OAI.PartitionPilot.Forcing.ExternalColumnCode.entries_increasing line 410
  25. theorem OAI.PartitionPilot.Forcing.externalOwnerHeightGraph_strictLex line 419
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalTileSlotSupports_mem line 472