OAI/SetTheory/PartitionPrinciple/Definability/CodedInjectiveCones.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.GraphDiagonalCode line 14
  2. def OAI.PartitionPilot.Forcing.GraphCompositionCode line 17
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.graphDiagonalFormula line 23
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_graphDiagonalFormula line 27
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.graphCompositionFormula line 40
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_graphCompositionFormula line 45
  7. def OAI.PartitionPilot.Forcing.identityFunctionGraph line 69
  8. theorem OAI.PartitionPilot.Forcing.mem_identityFunctionGraph line 72
  9. theorem OAI.PartitionPilot.Forcing.pair_mem_identityFunctionGraph line 83
  10. theorem OAI.PartitionPilot.Forcing.identityFunctionGraph_injection line 93
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.identityFunctionGraph_mem line 99
  12. structure OAI.PartitionPilot.Forcing.CodedDirectSystem line 129
  13. def OAI.PartitionPilot.Forcing.CodedDirectSystem.Related line 141
  14. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.map_entry_bounds line 145
  15. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.map_entry_total line 150
  16. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.map_identity_entry line 155
  17. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.map_comp_entry line 160
  18. theorem OAI.PartitionPilot.Forcing.GraphDiagonalCode.eq_identityFunctionGraph line 177
  19. theorem OAI.PartitionPilot.Forcing.graphDiagonalCode_identity line 192
  20. theorem OAI.PartitionPilot.Forcing.GraphCompositionCode.eq_relationCompose line 195
  21. theorem OAI.PartitionPilot.Forcing.graphCompositionCode_relationCompose line 211
  22. theorem OAI.PartitionPilot.Forcing.relationCompose_assoc line 230
  23. theorem OAI.PartitionPilot.Forcing.relationCompose_identity_left line 247
  24. theorem OAI.PartitionPilot.Forcing.relationCompose_identity_right line 261
  25. structure OAI.PartitionPilot.Forcing.CodedDirectPresentation line 282
  26. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.key_mem line 298
  27. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.exists_key line 302
  28. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.label_mem line 305
  29. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.label_cases line 309
  30. theorem OAI.PartitionPilot.Forcing.CodedDirectPresentation.map_lookup line 316
  31. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_bounds line 334
  32. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_refl line 339
  33. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_symm line 343
  34. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_trans line 348
  35. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_same_iff line 364
  36. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_same_iff_eq line 372
  37. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_of_entry line 377
  38. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_iff_entry line 381
  39. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_map_left_iff line 391
  40. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_map_right_iff line 398
  41. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.related_iff_common_images line 405
  42. structure OAI.PartitionPilot.Forcing.CodedDirectSystem.InjectiveCone line 419
  43. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.InjectiveCone.entry_bounds line 431
  44. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.InjectiveCone.entry_total line 435
  45. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.InjectiveCone.later_entry_iff line 440
  46. theorem OAI.PartitionPilot.Forcing.CodedDirectSystem.InjectiveCone.entry_eq_iff_related line 457
  47. def OAI.PartitionPilot.Forcing.CodedDirectSystem.InjectiveCone.Covers line 474