OAI/SetTheory/PartitionPrinciple/Definability/IndexedAttachmentCodes.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.attachmentIdeal line 11
  2. def OAI.PartitionPilot.Forcing.freshPart line 14
  3. theorem OAI.PartitionPilot.Forcing.mem_attachmentIdeal line 17
  4. theorem OAI.PartitionPilot.Forcing.mem_freshPart line 21
  5. theorem OAI.PartitionPilot.Forcing.attachmentIdeal_union_freshPart line 25
  6. theorem OAI.PartitionPilot.Forcing.attachmentIdeal_not_freshPart line 35
  7. def OAI.PartitionPilot.Forcing.attachmentShadowGraph line 40
  8. theorem OAI.PartitionPilot.Forcing.mem_attachmentShadowGraph line 45
  9. theorem OAI.PartitionPilot.Forcing.pair_mem_attachmentShadowGraph line 54
  10. theorem OAI.PartitionPilot.Forcing.meet_entry_in_attachmentIdeal line 66
  11. theorem OAI.PartitionPilot.Forcing.meet_entry_eq_of_attachmentIdeal line 73
  12. theorem OAI.PartitionPilot.Forcing.attachmentShadowGraph_function line 81
  13. theorem OAI.PartitionPilot.Forcing.attachmentShadowGraph_on_ideal line 101
  14. def OAI.PartitionPilot.Forcing.familyPointBound line 120
  15. theorem OAI.PartitionPilot.Forcing.mem_familyPointBound_of_entry line 122
  16. def OAI.PartitionPilot.Forcing.indexedAttachmentDomain line 126
  17. def OAI.PartitionPilot.Forcing.indexedAttachmentFresh line 131
  18. theorem OAI.PartitionPilot.Forcing.indexedAttachmentDomain_subset line 138
  19. theorem OAI.PartitionPilot.Forcing.indexedAttachmentFresh_subset line 142
  20. theorem OAI.PartitionPilot.Forcing.mem_indexedAttachmentDomain line 146
  21. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedAttachmentDomain line 158
  22. theorem OAI.PartitionPilot.Forcing.mem_indexedAttachmentFresh line 169
  23. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedAttachmentFresh line 185
  24. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedAttachmentDomain_of_entry line 197
  25. theorem OAI.PartitionPilot.Forcing.pair_mem_indexedAttachmentFresh_of_entries line 207