OAI/SetTheory/PartitionPrinciple/Definability/GroundFlatCopyGraphs.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.relationImage line 10
  2. theorem OAI.PartitionPilot.Forcing.mem_relationImage line 13
  3. def OAI.PartitionPilot.Forcing.relationConverse line 16
  4. theorem OAI.PartitionPilot.Forcing.mem_relationConverse line 20
  5. theorem OAI.PartitionPilot.Forcing.pair_mem_relationConverse line 29
  6. def OAI.PartitionPilot.Forcing.relationCompose line 40
  7. theorem OAI.PartitionPilot.Forcing.mem_relationCompose line 44
  8. theorem OAI.PartitionPilot.Forcing.pair_mem_relationCompose line 53
  9. theorem OAI.PartitionPilot.Forcing.relationImage_restrict line 64
  10. theorem OAI.PartitionPilot.Forcing.InjectionCode.converse_image line 77
  11. theorem OAI.PartitionPilot.Forcing.InjectionCode.compose line 95
  12. theorem OAI.PartitionPilot.Forcing.disjointFunction_union line 122
  13. theorem OAI.PartitionPilot.Forcing.disjointInjection_union line 146
  14. theorem OAI.PartitionPilot.Forcing.relationImage_union_graph line 160
  15. theorem OAI.PartitionPilot.Forcing.relationImage_source_selection line 182
  16. theorem OAI.PartitionPilot.Forcing.relationImage_source_union line 193
  17. theorem OAI.PartitionPilot.Forcing.disjointRelationImage_selection line 210
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.imageMemberFormula line 234
  19. def OAI.PartitionPilot.Forcing.BoundedFormula.converseEntryFormula line 237
  20. def OAI.PartitionPilot.Forcing.BoundedFormula.composeEntryFormula line 241
  21. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_imageMemberFormula line 247
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_converseEntryFormula line 252
  23. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_composeEntryFormula line 259
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.bounded_separation_mem line 274
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationImage_mem line 288
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationConverse_mem line 302
  27. theorem OAI.PartitionPilot.Forcing.TransitiveGround.relationCompose_mem line 320
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.groundEmbeddable_image line 338
  29. theorem OAI.PartitionPilot.Forcing.relationImage_commuting_square line 363
  30. def OAI.PartitionPilot.Forcing.flatCopyOrderGraph line 401
  31. def OAI.PartitionPilot.Forcing.flatCopyActionGraph line 407
  32. theorem OAI.PartitionPilot.Forcing.mem_flatCopyOrderGraph line 413
  33. theorem OAI.PartitionPilot.Forcing.mem_flatCopyActionGraph line 424
  34. theorem OAI.PartitionPilot.Forcing.pair_mem_flatCopyOrderGraph line 436
  35. theorem OAI.PartitionPilot.Forcing.pair_mem_flatCopyActionGraph line 448
  36. def OAI.PartitionPilot.Forcing.BoundedFormula.flatCopyOrderEntryFormula line 464
  37. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_flatCopyOrderEntryFormula line 471
  38. def OAI.PartitionPilot.Forcing.BoundedFormula.flatCopyActionEntryFormula line 479
  39. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_flatCopyActionEntryFormula line 486
  40. def OAI.PartitionPilot.Forcing.SetFormula.relationCompositionCodeFormula line 501
  41. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_relationCompositionCodeFormula line 513
  42. def OAI.PartitionPilot.Forcing.TransitiveGround.definable_relationCompose line 525
  43. def OAI.PartitionPilot.Forcing.functionGraphRange line 542
  44. theorem OAI.PartitionPilot.Forcing.mem_functionGraphRange line 545
  45. theorem OAI.PartitionPilot.Forcing.functionGraphRange_function line 550
  46. theorem OAI.PartitionPilot.Forcing.functionGraphRange_rank_le line 557
  47. theorem OAI.PartitionPilot.Forcing.TransitiveGround.functionGraphRange_mem line 567
  48. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyOrderGraph_mem line 589
  49. theorem OAI.PartitionPilot.Forcing.TransitiveGround.flatCopyActionGraph_mem line 608