OAI/SetTheory/PartitionPrinciple/Geometry/GroundBatchEmbeddingRecognition.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.withAux line 13
  2. def OAI.PartitionPilot.Forcing.GroundDefinableFunction.withAuxFamily line 40
  3. def OAI.PartitionPilot.Forcing.SetFormula.indexedDomainSetFormula line 83
  4. def OAI.PartitionPilot.Forcing.SetFormula.batchTemplateSetFormula line 87
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_indexedDomainSetFormula line 103
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_batchTemplateSetFormula line 123
  7. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_sUnion line 161
  8. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_doubleUnion line 168
  9. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_taggedExtension line 177
  10. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_canonicalMeet line 184
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_recursiveIndices line 191
  12. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_codedAttachmentOrder line 200
  13. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_pairSecondField line 213
  14. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_indexedFresh line 224
  15. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_batchInside line 235
  16. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_batchUpper line 245
  17. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_batchShadow line 257
  18. theorem OAI.PartitionPilot.Forcing.batchTemplateGraph_eq_section line 275

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

  19. def OAI.PartitionPilot.Forcing.TransitiveGround.batchEmbeddingFamily line 285
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.batchEmbeddingFamily_spec line 290
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_batchAttachment_embedding_family line 310
  22. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_liftedCompressionFamily line 347
  23. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_indexedDomain line 390
  24. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_batchTemplate line 400
  25. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_indexedSections line 434
  26. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_batchEmbeddingFamily line 442
  27. def OAI.PartitionPilot.Forcing.TransitiveGround.batchEmbeddingFamilyFormula line 466
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_batchEmbeddingFamilyFormula line 473