OAI/SetTheory/PartitionPrinciple/Geometry/GroundAttachmentEmbeddings.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taggedExtension_mem line 14
  2. def OAI.PartitionPilot.Forcing.BoundedFormula.attachmentShadowEntryFormula line 36
  3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_attachmentShadowEntryFormula line 43
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.attachmentIdeal_mem line 59
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.freshPart_mem line 75
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.attachmentShadowGraph_mem line 92
  7. def OAI.PartitionPilot.Forcing.attachmentOldEmbeddingGraph line 121
  8. def OAI.PartitionPilot.Forcing.attachmentFreshEmbeddingGraph line 124
  9. def OAI.PartitionPilot.Forcing.attachmentTemplateEmbeddingGraph line 128
  10. theorem OAI.PartitionPilot.Forcing.mem_attachmentOldEmbeddingGraph line 131
  11. theorem OAI.PartitionPilot.Forcing.pair_mem_attachmentOldEmbeddingGraph line 138
  12. theorem OAI.PartitionPilot.Forcing.attachmentOldEmbeddingGraph_isFunc line 148
  13. theorem OAI.PartitionPilot.Forcing.attachmentOldEmbeddingGraph_injection line 158
  14. theorem OAI.PartitionPilot.Forcing.mem_attachmentFreshEmbeddingGraph line 165
  15. theorem OAI.PartitionPilot.Forcing.pair_mem_attachmentFreshEmbeddingGraph line 173
  16. theorem OAI.PartitionPilot.Forcing.mem_attachmentTemplateEmbeddingGraph line 183
  17. theorem OAI.PartitionPilot.Forcing.pair_mem_attachmentTemplateEmbeddingGraph line 188
  18. theorem OAI.PartitionPilot.Forcing.attachmentTemplateEmbeddingGraph_of_ideal line 193
  19. theorem OAI.PartitionPilot.Forcing.attachmentTemplateEmbeddingGraph_of_fresh line 199
  20. theorem OAI.PartitionPilot.Forcing.attachmentTemplateEmbeddingGraph_isFunc line 211
  21. theorem OAI.PartitionPilot.Forcing.attachmentTemplateEmbeddingGraph_injection line 233
  22. def OAI.PartitionPilot.Forcing.BoundedFormula.attachmentOldEmbeddingEntryFormula line 256
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.attachmentFreshEmbeddingEntryFormula line 259
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_attachmentOldEmbeddingEntryFormula line 264
  25. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_attachmentFreshEmbeddingEntryFormula line 271
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.attachmentOldEmbeddingGraph_mem line 294
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.attachmentFreshEmbeddingGraph_mem line 313
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.attachmentTemplateEmbeddingGraph_mem line 334