OAI/SetTheory/PartitionPrinciple/Geometry/SeparationTileCodes.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.singleAttachmentLe line 10
  2. def OAI.PartitionPilot.Forcing.singleAttachmentOrder line 18
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_singleAttachmentOrder line 23
  4. theorem OAI.PartitionPilot.Forcing.singleAttachmentOrder_shape line 34
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.attachmentTagFormula line 43
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.attachmentOldNewFormula line 46
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.attachmentNewNewFormula line 52
  8. def OAI.PartitionPilot.Forcing.BoundedFormula.singleAttachmentLeFormula line 58
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.singleAttachmentOrderEntryFormula line 64
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_singleAttachmentLeFormula line 70
  11. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_singleAttachmentOrderEntryFormula line 80
  12. def OAI.PartitionPilot.Forcing.codedAttachmentFreshLe line 96
  13. def OAI.PartitionPilot.Forcing.codedAttachmentLe line 100
  14. def OAI.PartitionPilot.Forcing.codedAttachmentOrder line 108
  15. theorem OAI.PartitionPilot.Forcing.pair_mem_codedAttachmentOrder line 113
  16. theorem OAI.PartitionPilot.Forcing.codedAttachmentOrder_shape line 124
  17. def OAI.PartitionPilot.Forcing.BoundedFormula.codedAttachmentFreshLeFormula line 132
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.codedAttachmentLeFormula line 137
  19. def OAI.PartitionPilot.Forcing.BoundedFormula.codedAttachmentOrderEntryFormula line 149
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_codedAttachmentFreshLeFormula line 155
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_codedAttachmentLeFormula line 163
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_codedAttachmentOrderEntryFormula line 172
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.singleAttachmentOrder_mem line 193
  24. def OAI.PartitionPilot.Forcing.BoundedFormula.greatestLowerBoundFormula line 232
  25. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_greatestLowerBoundFormula line 237
  26. def OAI.PartitionPilot.Forcing.BoundedFormula.canonicalMeetEntryFormula line 245
  27. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_canonicalMeetEntryFormula line 250
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.canonicalMeetGraph_mem line 264
  29. structure OAI.PartitionPilot.Forcing.CodedPrincipalTile line 295
  30. abbrev OAI.PartitionPilot.Forcing.CodedPrincipalTile.Nodes line 307
  31. def OAI.PartitionPilot.Forcing.CodedPrincipalTile.encode line 309
  32. abbrev OAI.PartitionPilot.Forcing.CodedPrincipalTile.carrier line 313
  33. abbrev OAI.PartitionPilot.Forcing.CodedPrincipalTile.order line 315
  34. abbrev OAI.PartitionPilot.Forcing.CodedPrincipalTile.meetGraph line 318
  35. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.fresh_mem line 323
  36. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.shadow_entry line 326
  37. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encode_mem line 335
  38. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encode_injective line 340
  39. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encode_surjective line 356
  40. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.fresh_lower_iff line 364
  41. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.le_encode line 369
  42. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.partialOrder line 443
  43. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encoded_meet_glb line 460
  44. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.meetOrder line 470
  45. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encoded_meet_entry line 477
  46. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encoded_embedding_order_iff line 497
  47. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.encoded_embedding_code line 514
  48. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.old_embedding_code line 555
  49. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.template_entry line 562
  50. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.template_embedding_code line 575
  51. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.template_entry_iff line 581
  52. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.template_old_overlap line 592
  53. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.old_ideal line 602
  54. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.template_ideal line 606
  55. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.ground_codes line 623
  56. theorem OAI.PartitionPilot.Forcing.CodedPrincipalTile.exists_ground_tile line 642
  57. def OAI.PartitionPilot.Forcing.separationTileBase line 668
  58. def OAI.PartitionPilot.Forcing.separationTileCarrier line 671
  59. def OAI.PartitionPilot.Forcing.separationTileOrder line 674
  60. def OAI.PartitionPilot.Forcing.separationTileMeet line 678
  61. def OAI.PartitionPilot.Forcing.separationTileMap line 681
  62. theorem OAI.PartitionPilot.Forcing.separationTileBase_function line 684
  63. theorem OAI.PartitionPilot.Forcing.separationTileCoding line 694
  64. theorem OAI.PartitionPilot.Forcing.pair_mem_separationTileMap line 703
  65. theorem OAI.PartitionPilot.Forcing.separationTile_meetOrder line 711
  66. theorem OAI.PartitionPilot.Forcing.separationTile_embeddings line 717
  67. theorem OAI.PartitionPilot.Forcing.separationTile_exact_overlap line 726
  68. theorem OAI.PartitionPilot.Forcing.TransitiveGround.separationTile_ground line 738