OAI/SetTheory/PartitionPrinciple/Geometry/GroundCompressionOrigins.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.NatUnionCode.injection line 15
  2. theorem OAI.PartitionPilot.Forcing.NatUnionCode.meetEmbedding line 26
  3. theorem OAI.PartitionPilot.Forcing.NatUnionCode.shift line 61
  4. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_iterate_codes line 92
  5. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_iterate_graphs_mono line 106
  6. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.canonical_iterate_profile line 164
  7. structure OAI.PartitionPilot.Forcing.GroundCompressionUnionData line 215
  8. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.exists_groundUnion line 236
  9. theorem OAI.PartitionPilot.Forcing.rank_taggedExtension_lt line 288
  10. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.fresh_rank_lt line 299
  11. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.currentCarrier_rank_lt line 309
  12. theorem OAI.PartitionPilot.Forcing.RecursiveTemplateConstancy.iterate_carrier_ranks line 314
  13. theorem OAI.PartitionPilot.Forcing.NatUnionCode.rank_le line 330
  14. theorem OAI.PartitionPilot.Forcing.GroundCompressionUnionData.carrier_rank_le line 342
  15. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_original_subset line 365
  16. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_order_iff line 376
  17. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_meet_iff line 385
  18. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_action_iff line 393
  19. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_original_order_iff line 400
  20. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_original_meet_iff line 406
  21. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_original_action_iff line 412
  22. structure OAI.PartitionPilot.Forcing.GroundCompressionHeightData line 425
  23. structure OAI.PartitionPilot.Forcing.CompressionOriginalData line 451
  24. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_original_agreement line 475
  25. theorem OAI.PartitionPilot.Forcing.GroundCompressionState.union_original_data line 503
  26. theorem OAI.PartitionPilot.Forcing.ExternalRectangleCode.lift_compression line 519
  27. theorem OAI.PartitionPilot.Forcing.externalRectangles_subset_compression line 539
  28. structure OAI.PartitionPilot.Forcing.GroundCompressionOrigin line 553
  29. theorem OAI.PartitionPilot.Forcing.GroundCompressionOrigin.union_original_data line 566