OAI/SetTheory/PartitionPrinciple/Definability/GroundSelectedSupportTupleFamilies.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.TransitiveGround.internalRowTupleName line 17
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowTupleName_action line 34
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowTupleName_supported line 54
  4. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowTupleName_hs line 70
  5. def OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowNameGraph line 104
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_binaryRowNameGraph line 108
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_binaryRowNameGraph line 116
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowNameGraph_function line 128
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowNameGraph_mem line 141
  10. def OAI.PartitionPilot.Forcing.rowTupleCode line 183
  11. def OAI.PartitionPilot.Forcing.rowTupleFamily line 186
  12. theorem OAI.PartitionPilot.Forcing.pair_mem_rowTupleFamily line 189
  13. theorem OAI.PartitionPilot.Forcing.rowTupleFamily_function line 200
  14. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_rowTupleCode line 220
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowTupleFamily_mem line 234
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowTupleFamily_mem line 243
  17. theorem OAI.PartitionPilot.Forcing.Name.mem_indexedTuple_code line 265
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowTupleCode_eq line 280
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowTupleCode_eq line 308
  20. def OAI.PartitionPilot.Forcing.rowTupleTerms line 344
  21. theorem OAI.PartitionPilot.Forcing.mem_rowTupleTerms line 347
  22. theorem OAI.PartitionPilot.Forcing.rowTupleTerms_function line 357
  23. theorem OAI.PartitionPilot.Forcing.rowTupleTerms_surjective line 361
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowTupleTerms_mem line 369
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowTupleTerms_below line 376
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowTupleTerms_mem_below line 388
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowTupleName_mem line 421
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundSupportTupleFamily line 471