OAI/SetTheory/PartitionPrinciple/Definability/PresentedGroupCodes.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.Truth line 14
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_imp line 21
  3. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_disj line 26
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exMem line 31
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_toFormula line 36
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.absolute line 56
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.emptyFormula line 72
  8. def OAI.PartitionPilot.Forcing.BoundedFormula.successorFormula line 75
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.setTransitiveFormula line 79
  10. def OAI.PartitionPilot.Forcing.BoundedFormula.zeroOrSuccessorFormula line 82
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.naturalFormula line 85
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_emptyFormula line 89
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_successorFormula line 98
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_setTransitiveFormula line 114
  15. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_zeroOrSuccessorFormula line 117
  16. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_naturalFormula line 123
  17. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_naturalFormula line 128
  18. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_singletonFormula line 138
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_unorderedPairFormula line 151
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_orderedPairFormula line 168
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_pairMembershipFormula line 194
  22. def OAI.PartitionPilot.Forcing.SetFormula.exactSetFormula line 214
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_exactSetFormula line 224
  24. def OAI.PartitionPilot.Forcing.BoundedFormula.ordinalFormula line 260
  25. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_ordinalFormula line 263
  26. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_ordinalFormula line 268
  27. def OAI.PartitionPilot.Forcing.BoundedFormula.graphFiberInclusionFormula line 281
  28. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_graphFiberInclusionFormula line 286
  29. def OAI.PartitionPilot.Forcing.BoundedFormula.graphFiberEqualityFormula line 301
  30. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_graphFiberEqualityFormula line 304
  31. structure OAI.PartitionPilot.Forcing.PartialOrderCode line 319
  32. def OAI.PartitionPilot.Forcing.BoundedFormula.relationOnFormula line 330
  33. def OAI.PartitionPilot.Forcing.BoundedFormula.reflexiveFormula line 333
  34. def OAI.PartitionPilot.Forcing.BoundedFormula.antisymmetricFormula line 336
  35. def OAI.PartitionPilot.Forcing.BoundedFormula.transitiveFormula line 340
  36. def OAI.PartitionPilot.Forcing.BoundedFormula.partialOrderFormula line 345
  37. def OAI.PartitionPilot.Forcing.BoundedFormula.topFormula line 349
  38. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_relationOnFormula line 352
  39. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_partialOrderFormula line 357
  40. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_topFormula line 369
  41. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_partialOrderCode line 381
  42. theorem OAI.PartitionPilot.Forcing.TransitiveGround.partialOrderCode_absolute line 387
  43. def OAI.PartitionPilot.Forcing.BoundedFormula.orderedTripleFormula line 404
  44. def OAI.PartitionPilot.Forcing.BoundedFormula.tripleMembershipFormula line 408
  45. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_orderedTripleFormula line 411
  46. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_tripleMembershipFormula line 426
  47. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_relationBetweenFormula line 443
  48. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_functionFormula line 448
  49. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_functionCode line 474
  50. def OAI.PartitionPilot.Forcing.BoundedFormula.nestedActionTripleFormula line 491
  51. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_nestedActionTripleFormula line 500
  52. def OAI.PartitionPilot.Forcing.BoundedFormula.binaryRelationFormula line 529
  53. def OAI.PartitionPilot.Forcing.BoundedFormula.binaryFunctionFormula line 533
  54. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_binaryRelationFormula line 539
  55. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_binaryFunctionFormula line 552
  56. structure OAI.PartitionPilot.Forcing.GroupCode line 580
  57. def OAI.PartitionPilot.Forcing.BoundedFormula.groupIdentityFormula line 595
  58. def OAI.PartitionPilot.Forcing.BoundedFormula.groupInverseFormula line 599
  59. def OAI.PartitionPilot.Forcing.BoundedFormula.groupAssociativeFormula line 603
  60. def OAI.PartitionPilot.Forcing.BoundedFormula.groupFormula line 611
  61. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_groupFormula line 616
  62. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_groupCode line 638
  63. theorem OAI.PartitionPilot.SetRealization.Presentation.groupCode line 657