OAI/SetTheory/PartitionPrinciple/Forcing/IndexedTupleNames.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_checkState_fixedPoint line 12
  2. theorem OAI.PartitionPilot.Forcing.TransitiveGround.exists_groundCheck_certificate line 32
  3. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_uniformCheckFormula line 78
  4. def OAI.PartitionPilot.Forcing.SetFormula.checkEntryFormula line 110
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_checkEntryFormula line 123
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.check_mem line 152
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.ground_subset_symmetric_values line 201
  8. def OAI.PartitionPilot.Forcing.pairNameCode line 223
  9. def OAI.PartitionPilot.Forcing.orderedPairNameCode line 226
  10. theorem OAI.PartitionPilot.Forcing.Name.orderedPair_code line 232
  11. def OAI.PartitionPilot.Forcing.SetFormula.pairNameCodeFormula line 253
  12. def OAI.PartitionPilot.Forcing.SetFormula.orderedPairNameCodeFormula line 258
  13. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pairNameCode_mem line 268
  14. theorem OAI.PartitionPilot.Forcing.TransitiveGround.orderedPairNameCode_mem line 273
  15. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_pairNameCodeFormula line 279
  16. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_orderedPairNameCodeFormula line 307
  17. def OAI.PartitionPilot.Forcing.checkCodePresentation line 341
  18. def OAI.PartitionPilot.Forcing.checkNameCode line 349
  19. theorem OAI.PartitionPilot.Forcing.Name.check_code_eq line 354
  20. def OAI.PartitionPilot.Forcing.SetFormula.checkNameCodeFormula line 373
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.checkNameCode_mem line 381
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_checkNameCodeFormula line 390
  23. def OAI.PartitionPilot.Forcing.Name.indexedGraphName line 413
  24. theorem OAI.PartitionPilot.Forcing.Name.mem_indexedGraphName_code line 418
  25. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_indexedGraphName line 433
  26. theorem OAI.PartitionPilot.Forcing.Name.pair_mem_eval_indexedGraphName line 446
  27. theorem OAI.PartitionPilot.Forcing.Name.eval_indexedGraphName_function line 460
  28. def OAI.PartitionPilot.Forcing.SetFormula.indexedGraphValueFormula line 479
  29. def OAI.PartitionPilot.Forcing.SetFormula.indexedGraphNameEntryFormula line 484
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_indexedGraphValueFormula line 500
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_indexedGraphNameEntryFormula line 537
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.indexedGraphName_mem line 566
  33. def OAI.PartitionPilot.Forcing.orderedPairNameFamily line 621
  34. theorem OAI.PartitionPilot.Forcing.mem_orderedPairNameFamily line 624
  35. theorem OAI.PartitionPilot.Forcing.pairNameCode_subset line 634
  36. def OAI.PartitionPilot.Forcing.iteratedPairNameFamily line 641
  37. theorem OAI.PartitionPilot.Forcing.iteratedPairNameFamily_zero line 645
  38. theorem OAI.PartitionPilot.Forcing.iteratedPairNameFamily_succ line 648
  39. theorem OAI.PartitionPilot.Forcing.Name.inputFunction line 663
  40. theorem OAI.PartitionPilot.Forcing.Name.inputValue line 666
  41. theorem OAI.PartitionPilot.Forcing.Name.inputValid line 672
  42. def OAI.PartitionPilot.Forcing.Name.inputEvaluationName line 677
  43. theorem OAI.PartitionPilot.Forcing.Name.inputEvaluationName_entry line 680
  44. theorem OAI.PartitionPilot.Forcing.TransitiveGround.inputEvaluationName_mem line 705
  45. def OAI.PartitionPilot.Forcing.namePool line 727
  46. theorem OAI.PartitionPilot.Forcing.mem_namePool line 730
  47. theorem OAI.PartitionPilot.Forcing.TransitiveGround.namePool_mem line 735
  48. theorem OAI.PartitionPilot.Forcing.Name.child_mem_namePool line 760
  49. theorem OAI.PartitionPilot.Forcing.Name.indexedGraphName_covers_eval line 764
  50. def OAI.PartitionPilot.Forcing.Name.indexedTuple line 790
  51. theorem OAI.PartitionPilot.Forcing.Name.indexedGraphName_eq_indexedTuple line 794
  52. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_indexedTuple line 799
  53. theorem OAI.PartitionPilot.Forcing.Name.pair_mem_eval_indexedTuple line 806
  54. theorem OAI.PartitionPilot.Forcing.Name.eval_indexedTuple_function line 818
  55. theorem OAI.PartitionPilot.Forcing.Name.eval_indexedTuple_domain_eq line 832
  56. theorem OAI.PartitionPilot.Forcing.Name.eval_indexedTuple_eq_iff line 853
  57. theorem OAI.PartitionPilot.Forcing.Name.rename_indexedTuple line 868
  58. theorem OAI.PartitionPilot.Forcing.Name.act_indexedTuple line 877
  59. theorem OAI.PartitionPilot.Forcing.Name.indexedTuple_supported line 884
  60. theorem OAI.PartitionPilot.Forcing.Name.indexedTuple_hs line 893