OAI/SetTheory/PartitionPrinciple/Geometry/GroundBatchAttachment.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encoded_embedding_order_iff line 12
  2. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.encoded_embedding_code line 29
  3. theorem OAI.PartitionPilot.Forcing.CodedTemplateAttachment.old_embedding_code line 70
  4. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_graph_entry line 86
  5. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_graph_entry_iff line 100
  6. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_embedding_code line 111
  7. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_order_iff line 117
  8. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_old_agreement line 125
  9. def OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchFreshNode line 141
  10. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_old_lower_iff line 145
  11. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_old_upper_iff line 153
  12. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_cross_lower_iff line 158
  13. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_shadow_meet_code line 168
  14. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_cross_meet_code line 185
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchAttachment_ground_codes line 216
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_batchAttachment line 239