OAI/SetTheory/PartitionPrinciple/Definability/GroundLiftedRowTupleProvenance.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.pairedGraph line 13
  2. theorem OAI.PartitionPilot.Forcing.mem_pairedGraph line 18
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_pairedGraph line 27
  4. theorem OAI.PartitionPilot.Forcing.pairedGraph_eq line 40
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.pairedGraphEntryFormula line 61
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_pairedGraphEntryFormula line 67
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairedGraph_mem line 78
  8. theorem OAI.PartitionPilot.SetRealization.Presentation.recode_subset line 108
  9. theorem OAI.PartitionPilot.SetRealization.Presentation.product_identity_graph line 123
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recode_subset_mem line 159
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.product_identity_graph_mem line 167
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recode_conditionOrder_mem line 175
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.recode_actionGraph_mem line 183
  14. def OAI.PartitionPilot.SetRealization.Presentation.pairEmpty line 208
  15. theorem OAI.PartitionPilot.SetRealization.Presentation.pairEmpty_forwardGraph line 222
  16. theorem OAI.PartitionPilot.SetRealization.Presentation.pairEmpty_inverseGraph line 242
  17. theorem OAI.PartitionPilot.SetRealization.Presentation.pairEmpty_order_iff line 259
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_carrier_mem line 275
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_forwardGraph_mem line 281
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_inverseGraph_mem line 290
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_order_mem line 296
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_actionGraph_mem line 302
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairEmpty_conditionMapFamily_mem line 321
  24. def OAI.PartitionPilot.Forcing.liftedRowTupleFamily line 338
  25. theorem OAI.PartitionPilot.Forcing.pair_mem_liftedRowTupleFamily line 346
  26. theorem OAI.PartitionPilot.Forcing.liftedRowTupleFamily_function line 364
  27. theorem OAI.PartitionPilot.Forcing.liftedRowTupleFamily_surjective line 368
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.liftedRowTupleFamily_mem line 384
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.binaryLiftedRowTupleFamily_mem line 399