OAI/SetTheory/PartitionPrinciple/Geometry/GroundConstantBatchLayers.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.batchTemplateGraph_eq_section line 11

    Distinct definitions of this name: OAI/SetTheory/PartitionPrinciple/Geometry/GroundBatchEmbeddingRecognition.lean:275 (same statement text; different proof or body). Qualify references as OAI.PartitionPilot.Forcing.batchTemplateGraph_eq_section@path.

  2. def OAI.PartitionPilot.Forcing.TransitiveGround.batchTemplateFamily line 27
  3. def OAI.PartitionPilot.Forcing.TransitiveGround.batchTemplateFamilyBound line 32
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchTemplateFamily_spec line 36
  5. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchIncomingFiber line 64
  6. abbrev OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchIncomingComponents line 65
  7. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchIncomingFiber_eq line 68
  8. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchIncomingComponents_function line 79
  9. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchIncomingComponents_encode line 84
  10. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchIncomingComponents_ground line 98
  11. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchSeparatedLayerCode line 108
  12. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.batchSeparatedWitness line 156
  13. def OAI.PartitionPilot.Forcing.AttachmentBatchInputs.constantBatchLayerWitness line 186
  14. theorem OAI.PartitionPilot.Forcing.AttachmentBatchInputs.constantBatchLayerWitness_spec line 190