OAI/ModelTheory/Choiceless/Counting.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CPTSeparation.Counting.Structure line 13
  2. inductive OAI.CPTSeparation.Counting.Formula line 16
  3. def OAI.CPTSeparation.Counting.Formula.free line 30
  4. def OAI.CPTSeparation.Counting.Formula.eval line 39
  5. theorem OAI.CPTSeparation.Counting.Formula.eval_congr line 48
  6. theorem OAI.CPTSeparation.Counting.Formula.eval_of_bijectionSystem line 80
  7. def OAI.CPTSeparation.Counting.Formula.conjoin line 110
  8. theorem OAI.CPTSeparation.Counting.Formula.eval_conjoin line 114
  9. theorem OAI.CPTSeparation.Counting.Formula.free_conjoin_subset line 120
  10. def OAI.CPTSeparation.Counting.typeOf line 131
  11. theorem OAI.CPTSeparation.Counting.typeOf_eq_iff line 134
  12. theorem OAI.CPTSeparation.Counting.type_separator line 145
  13. theorem OAI.CPTSeparation.Counting.isolate_type line 158
  14. theorem OAI.CPTSeparation.Counting.extension_equiv line 206
  15. def OAI.CPTSeparation.Counting.Formula.rename line 238
  16. theorem OAI.CPTSeparation.Counting.Formula.free_rename line 247
  17. theorem OAI.CPTSeparation.Counting.Formula.eval_rename line 258
  18. theorem OAI.CPTSeparation.Counting.typeOf_project line 280
  19. theorem OAI.CPTSeparation.Counting.typeOf_congr line 288
  20. theorem OAI.CPTSeparation.Counting.typeOf_permute line 294
  21. theorem OAI.CPTSeparation.Counting.extension_bijection line 309
  22. theorem OAI.CPTSeparation.Counting.extend_type line 337
  23. def OAI.CPTSeparation.Counting.tupleNames line 370
  24. theorem OAI.CPTSeparation.Counting.mem_tupleNames line 373
  25. def OAI.CPTSeparation.Counting.tupleAssignment line 380
  26. theorem OAI.CPTSeparation.Counting.tupleAssignment_apply line 383
  27. def OAI.CPTSeparation.Counting.tupleType line 390
  28. theorem OAI.CPTSeparation.Counting.tupleType_assignment line 393
  29. theorem OAI.CPTSeparation.Counting.tupleType_project line 401
  30. theorem OAI.CPTSeparation.Counting.tupleType_extend line 431
  31. theorem OAI.CPTSeparation.Counting.tupleType_append line 484
  32. theorem OAI.CPTSeparation.Counting.eval_iso line 501
  33. theorem OAI.CPTSeparation.Counting.tupleType_iso line 518
  34. abbrev OAI.CPTSeparation.Grid.ClassLabel line 538
  35. instance OAI.CPTSeparation.Grid.(instance at line 542) line 542
  36. def OAI.CPTSeparation.Grid.classLabel line 547
  37. def OAI.CPTSeparation.Grid.classIndex line 551
  38. inductive OAI.CPTSeparation.Grid.AnalysisSymbol line 554
  39. def OAI.CPTSeparation.Grid.rawDifference line 560
  40. def OAI.CPTSeparation.Grid.analysisStructure line 564
  41. theorem OAI.CPTSeparation.Grid.classLabel_shiftLocal line 570
  42. theorem OAI.CPTSeparation.Grid.classLabel_shiftConfig line 574
  43. theorem OAI.CPTSeparation.Grid.AtomShift.classLabel line 579
  44. theorem OAI.CPTSeparation.Grid.AtomShift.analysisRelation line 583
  45. def OAI.CPTSeparation.Grid.predecessors line 598
  46. theorem OAI.CPTSeparation.Grid.predecessors_recovers_class line 600
  47. def OAI.CPTSeparation.Grid.classFormula line 619
  48. theorem OAI.CPTSeparation.Grid.free_classFormula line 622
  49. theorem OAI.CPTSeparation.Grid.eval_classFormula line 629
  50. theorem OAI.CPTSeparation.Grid.type_recovers_classes line 646
  51. abbrev OAI.CPTSeparation.Grid.Block line 657
  52. def OAI.CPTSeparation.Grid.atomBlock line 659
  53. def OAI.CPTSeparation.Grid.blockEdges line 663
  54. def OAI.CPTSeparation.Grid.touch line 667
  55. theorem OAI.CPTSeparation.Grid.blockEdges_card line 669
  56. theorem OAI.CPTSeparation.Grid.touch_card line 679
  57. theorem OAI.CPTSeparation.Grid.touch_shift line 681
  58. theorem OAI.CPTSeparation.Grid.AtomShift.congr line 684
  59. def OAI.CPTSeparation.Grid.touches line 703
  60. theorem OAI.CPTSeparation.Grid.touches_card line 706
  61. theorem OAI.CPTSeparation.Grid.touch_subset_touches line 713
  62. theorem OAI.CPTSeparation.Grid.touches_mono line 717
  63. theorem OAI.CPTSeparation.Grid.touches_insert_update line 723
  64. def OAI.CPTSeparation.Grid.HasState line 745
  65. theorem OAI.CPTSeparation.Grid.hasState_edge line 748
  66. theorem OAI.CPTSeparation.Grid.hasState_config line 756
  67. def OAI.CPTSeparation.Grid.stateAt line 767
  68. theorem OAI.CPTSeparation.Grid.stateAt_edge line 778
  69. theorem OAI.CPTSeparation.Grid.stateAt_config line 782
  70. theorem OAI.CPTSeparation.Grid.hasState_stateAt line 785
  71. theorem OAI.CPTSeparation.Grid.classLabel_edge_iff line 797
  72. theorem OAI.CPTSeparation.Grid.atomShift_of_states line 813
  73. abbrev OAI.CPTSeparation.Grid.Occurrences line 851
  74. def OAI.CPTSeparation.Grid.occurrenceAtom line 853
  75. def OAI.CPTSeparation.Grid.Augment line 856
  76. structure OAI.CPTSeparation.Grid.SameDiagram line 859
  77. theorem OAI.CPTSeparation.Grid.augmented_diagram_shift line 865
  78. theorem OAI.CPTSeparation.Grid.sameDiagram_of_type line 916
  79. theorem OAI.CPTSeparation.Grid.occurrences_card line 951
  80. theorem OAI.CPTSeparation.Grid.augment_card line 958
  81. def OAI.CPTSeparation.Grid.namesBelow line 963
  82. theorem OAI.CPTSeparation.Grid.namesBelow_spare line 966
  83. theorem OAI.CPTSeparation.Grid.tuple_partial_shift line 974
  84. theorem OAI.CPTSeparation.Grid.AtomShift.stateAt_flow line 985
  85. theorem OAI.CPTSeparation.Grid.AtomShift.unique_on_touch line 999