OAI/SetTheory/PartitionPrinciple/Models/GroundExternalWordQuotient.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PartitionPilot.Forcing.ExternalWordRewrite.WordQuotient line 14
  2. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.quotientMap line 16
  3. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.symbolValue line 19
  4. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.evalWord line 23
  5. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.atomic_eval line 25
  6. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.evalQuotient line 40
  7. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.evalQuotient_mk line 44
  8. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.oldClass line 47
  9. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.freeWordMap line 54
  10. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.freeWordMap_step line 57
  11. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.freeClass line 69
  12. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.freeClass_mk line 76
  13. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.fromExternal line 79
  14. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.fromExternal_old line 84
  15. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.fromExternal_free line 87
  16. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.fromExternal_evalWord line 90
  17. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.evalWord_signed_word line 101
  18. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.evalQuotient_fromExternal line 116
  19. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.fromExternal_evalQuotient line 139
  20. def OAI.PartitionPilot.Forcing.ExternalWordRewrite.quotientEquiv line 145
  21. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.path_iff_evalWord line 152
  22. theorem OAI.PartitionPilot.Forcing.ExternalWordRewrite.evalWord_surjective line 165
  23. def OAI.PartitionPilot.Forcing.TransitiveGround.externalWordEquivalence line 179
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalWordEquivalence_mem line 189
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalWordEquivalence_code line 197
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_externalWordEquivalence line 213
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_externalWordEquivalence_eval line 227
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_mem_externalWordEquivalence_congruence line 237
  29. def OAI.PartitionPilot.Forcing.TransitiveGround.externalWordQuotientPresentation line 246
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalWordQuotientPresentation_carrier line 254
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalWordQuotientPresentation_encode_mk line 260
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalWordClassifier_eq_graph line 268
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalWordQuotient_ground line 283