OAI/SetTheory/PartitionPrinciple/Forcing/GroundOutsideRowNames.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.smallFunctionActionGraph_mem line 19
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.smallFunction_conditionMapFamily_mem line 69
  3. def OAI.PartitionPilot.Forcing.rowUsedRows line 89
  4. theorem OAI.PartitionPilot.Forcing.mem_rowUsedRows line 92
  5. theorem OAI.PartitionPilot.Forcing.rowUsedRows_subset line 108
  6. theorem OAI.PartitionPilot.Forcing.row_mem_rowUsedRows line 111
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowUsedRows_mem line 123
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowUsedRows_groundEmbeddable line 133
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.countablePartialFunctions_rowSupport line 146
  10. def OAI.PartitionPilot.Forcing.columnOrder line 172
  11. def OAI.PartitionPilot.Forcing.rowCoordinatePresentation line 178
  12. def OAI.PartitionPilot.Forcing.PosetAction.rowCoordinates line 187
  13. theorem OAI.PartitionPilot.Forcing.PosetAction.rowCoordinates_apply line 193
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowCoordinate_carrier_mem line 208
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.rowCoordinate_graph_mem line 217
  16. def OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction line 240
  17. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction_entry line 252
  18. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowActionGraph_mem line 272
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowCondition_entry_shape line 298
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction_raw_entry line 321
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction_usedRows line 338
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction_eq_of_fixes_usedRows line 360
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction_eq_of_principalFix line 404
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowAction_usedRows_bounded line 417
  25. def OAI.PartitionPilot.Forcing.TransitiveGround.internalRowName line 449
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowName_action line 466
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowName_supported line 512
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowName_hs line 525
  29. def OAI.PartitionPilot.Forcing.TransitiveGround.internalRowSetName line 556
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowSetName_action line 573
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalRowSetName_hs line 612
  32. def OAI.PartitionPilot.Forcing.outsideRowIndices line 638
  33. theorem OAI.PartitionPilot.Forcing.outsideRowIndices_subset line 642
  34. theorem OAI.PartitionPilot.Forcing.encode_mem_outsideRowIndices line 646
  35. def OAI.PartitionPilot.Forcing.TransitiveGround.binaryRowSubsetName line 657
  36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.entry_binaryRowSubsetName line 663
  37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_binaryRowSubsetName_code line 678
  38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.eval_binaryRowSubsetName line 692
  39. theorem OAI.PartitionPilot.Forcing.TransitiveGround.eval_binaryRowSubsetName_subset line 712
  40. def OAI.PartitionPilot.Forcing.TransitiveGround.internalOutsideRowsName line 725
  41. theorem OAI.PartitionPilot.Forcing.TransitiveGround.entry_internalOutsideRowsName line 734
  42. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_eval_internalOutsideRowsName line 757
  43. theorem OAI.PartitionPilot.Forcing.TransitiveGround.eval_internalOutsideRowsName_subset line 781
  44. theorem OAI.PartitionPilot.Forcing.TransitiveGround.eval_internalOutsideRowsName_nonempty line 795
  45. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalOutsideRowsName_action line 818
  46. theorem OAI.PartitionPilot.Forcing.TransitiveGround.internalOutsideRowsName_hs line 859