OAI/SetTheory/PartitionPrinciple/Definability/TaggedSumPresentations.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.natSetCode_injective line 11
  2. theorem OAI.PartitionPilot.Forcing.natSetCode_mem_iff line 23
  3. theorem OAI.PartitionPilot.Forcing.mem_natSetCode line 31
  4. def OAI.PartitionPilot.Forcing.natPresentation line 41
  5. def OAI.PartitionPilot.Forcing.natInitialPresentation line 49
  6. theorem OAI.PartitionPilot.Forcing.natSetCode_finite line 58
  7. def OAI.PartitionPilot.Forcing.externalSignCode line 76
  8. theorem OAI.PartitionPilot.Forcing.externalSignCode_injective line 78
  9. theorem OAI.PartitionPilot.Forcing.mem_natTwo_iff_externalSignCode line 85
  10. def OAI.PartitionPilot.Forcing.externalActorSymbol line 97
  11. def OAI.PartitionPilot.Forcing.externalLetterSymbol line 99
  12. def OAI.PartitionPilot.Forcing.externalGeneratorAlphabet line 102
  13. theorem OAI.PartitionPilot.Forcing.externalActorSymbol_injective line 105
  14. theorem OAI.PartitionPilot.Forcing.externalLetterSymbol_inj line 108
  15. theorem OAI.PartitionPilot.Forcing.externalActorSymbol_ne_letterSymbol line 117
  16. theorem OAI.PartitionPilot.Forcing.mem_externalGeneratorAlphabet line 123
  17. theorem OAI.PartitionPilot.Forcing.externalActorSymbol_mem line 145
  18. theorem OAI.PartitionPilot.Forcing.externalLetterSymbol_mem line 155
  19. def OAI.PartitionPilot.Forcing.externalAlphabetEncode line 165
  20. theorem OAI.PartitionPilot.Forcing.externalAlphabetEncode_injective line 170
  21. def OAI.PartitionPilot.Forcing.externalGeneratorAlphabetPresentation line 185
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGeneratorAlphabet_mem line 206
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.finiteWordFormula line 233
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_finiteWordFormula line 236
  25. theorem OAI.PartitionPilot.Forcing.finiteWord_domain_unique line 245
  26. def OAI.PartitionPilot.Forcing.TransitiveGround.finiteWords line 263
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_finiteWords_iff line 267
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_finiteWords line 280
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWords_mem line 291
  30. theorem OAI.PartitionPilot.Compression.RecursiveMaps.RationalHeights.Fraction.intCode_surjective line 327
  31. def OAI.PartitionPilot.Forcing.fractionCarrier line 340
  32. def OAI.PartitionPilot.Forcing.fractionEncode line 343
  33. theorem OAI.PartitionPilot.Forcing.fractionEncode_mem line 346
  34. theorem OAI.PartitionPilot.Forcing.fractionEncode_injective line 353
  35. theorem OAI.PartitionPilot.Forcing.mem_fractionCarrier line 364
  36. def OAI.PartitionPilot.Forcing.fractionPresentation line 380
  37. def OAI.PartitionPilot.Forcing.fractionEquivGraph line 387
  38. def OAI.PartitionPilot.Forcing.fractionLtGraph line 392
  39. theorem OAI.PartitionPilot.Forcing.fractionEquivGraph_subset line 397
  40. theorem OAI.PartitionPilot.Forcing.fractionLtGraph_subset line 400
  41. theorem OAI.PartitionPilot.Forcing.pair_mem_fractionEquivGraph line 403
  42. theorem OAI.PartitionPilot.Forcing.pair_mem_fractionLtGraph line 416
  43. def OAI.PartitionPilot.Forcing.taggedSumCarrier line 438
  44. theorem OAI.PartitionPilot.Forcing.mem_taggedSumCarrier line 441
  45. def OAI.PartitionPilot.Forcing.taggedSumEncode line 453
  46. theorem OAI.PartitionPilot.Forcing.taggedSumEncode_injective line 457
  47. def OAI.PartitionPilot.Forcing.taggedSumPresentation line 466
  48. def OAI.PartitionPilot.Forcing.externalSignPresentation line 482
  49. theorem OAI.PartitionPilot.Forcing.TransitiveGround.taggedSumCarrier_mem line 496