OAI/SetTheory/PartitionPrinciple/Geometry/GroundExternalGenerators.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.externalActorSymbolGraph line 10
  2. def OAI.PartitionPilot.Forcing.externalGeneratorSymbolGraph line 15
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_externalActorSymbolGraph line 20
  4. theorem OAI.PartitionPilot.Forcing.pair_mem_externalGeneratorSymbolGraph line 31
  5. theorem OAI.PartitionPilot.Forcing.externalActorSymbolGraph_eq_graph line 42
  6. theorem OAI.PartitionPilot.Forcing.externalGeneratorSymbolGraph_eq_graph line 57
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.externalActorSymbolEntryFormula line 75
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalActorSymbolEntryFormula line 79
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.externalGeneratorSymbolEntryFormula line 89
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_externalGeneratorSymbolEntryFormula line 93
  11. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalActorSymbolGraph_mem line 110
  12. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGeneratorSymbolGraph_mem line 132
  13. def OAI.PartitionPilot.Forcing.singletonWordGraph line 166
  14. theorem OAI.PartitionPilot.Forcing.pair_mem_singletonWordGraph line 170
  15. def OAI.PartitionPilot.Forcing.BoundedFormula.singletonWordFormula line 182
  16. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_singletonWordFormula line 185
  17. def OAI.PartitionPilot.Forcing.BoundedFormula.singletonWordEntryFormula line 195
  18. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_singletonWordEntryFormula line 199
  19. theorem OAI.PartitionPilot.Forcing.TransitiveGround.singletonWordGraph_mem line 216
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.singletonWordGraph_eq_graph line 237
  21. theorem OAI.PartitionPilot.SetRealization.Presentation.relationCompose_graph line 267
  22. structure OAI.PartitionPilot.Forcing.GroundExternalGroupData line 297
  23. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroup_code_of_presentation line 315
  24. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroup_code line 330
  25. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGroupData line 341
  26. theorem OAI.PartitionPilot.Forcing.TransitiveGround.GroundExternalGroupData.realize_group line 349
  27. def OAI.PartitionPilot.Forcing.TransitiveGround.externalSymbolClasses line 369
  28. def OAI.PartitionPilot.Forcing.TransitiveGround.externalOldInclusion line 375
  29. def OAI.PartitionPilot.Forcing.TransitiveGround.externalChildGenerators line 379
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalSymbolClasses_mem line 389
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGeneratorGraphs_mem line 401
  32. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalSymbolClasses_eq_graph line 418
  33. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalOldInclusion_eq_graph line 440
  34. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalChildGenerators_eq_graph line 451
  35. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalOldInclusion_entry_iff line 462
  36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalChildGenerators_entry_iff line 470
  37. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGeneratorGraphs_injections line 479
  38. theorem OAI.PartitionPilot.Forcing.TransitiveGround.externalGeneratorGraphs_ground_injections line 494