OAI/SetTheory/PartitionPrinciple/Definability/GroundBatchAttachmentGraphs.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.batchAttachmentShadowGraph line 9
  2. def OAI.PartitionPilot.Forcing.batchAttachmentTemplateGraph line 18
  3. def OAI.PartitionPilot.Forcing.batchTemplateGraph line 27
  4. theorem OAI.PartitionPilot.Forcing.batchAttachmentShadowGraph_shape line 34
  5. theorem OAI.PartitionPilot.Forcing.pair_mem_batchAttachmentShadowGraph line 38
  6. theorem OAI.PartitionPilot.Forcing.batchAttachmentTemplateGraph_shape line 59
  7. theorem OAI.PartitionPilot.Forcing.pair_mem_batchAttachmentTemplateGraph line 66
  8. theorem OAI.PartitionPilot.Forcing.pair_mem_batchTemplateGraph line 91
  9. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_shadow_entry_iff line 111
  10. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_shadow_function line 126
  11. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_entry_iff line 138
  12. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_total line 161
  13. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_unique line 172
  14. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_function line 187
  15. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batch_template_fiber_function line 198
  16. def OAI.PartitionPilot.Forcing.BoundedFormula.batchShadowGraphFormula line 220
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_batchShadowGraphFormula line 230
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.batchTemplateGraphFormula line 241
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_batchTemplateGraphFormula line 247
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.batchTemplateFiberFormula line 257
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_batchTemplateFiberFormula line 260
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchAttachmentShadowGraph_mem line 275
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchAttachmentTemplateGraph_mem line 302
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchTemplateGraph_mem line 332