OAI/SetTheory/PartitionPrinciple/Forcing/OrbitPairGraphNames.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.Name.rename line 13
  2. theorem OAI.PartitionPilot.Forcing.Name.entry_rename line 18
  3. theorem OAI.PartitionPilot.Forcing.Name.rename_assemble line 29
  4. theorem OAI.PartitionPilot.Forcing.Name.rename_id line 44
  5. theorem OAI.PartitionPilot.Forcing.Name.rename_comp line 57
  6. theorem OAI.PartitionPilot.Forcing.Name.rename_empty line 73
  7. theorem OAI.PartitionPilot.Forcing.Name.rename_check line 83
  8. theorem OAI.PartitionPilot.Forcing.Name.rename_check_fixed line 92
  9. theorem OAI.PartitionPilot.Forcing.Name.rename_singleton line 96
  10. theorem OAI.PartitionPilot.Forcing.Name.rename_unorderedPair line 101
  11. theorem OAI.PartitionPilot.Forcing.Name.rename_orderedPair line 110
  12. theorem OAI.PartitionPilot.Forcing.Name.eval_rename line 117
  13. structure OAI.PartitionPilot.Forcing.PosetAction line 142
  14. def OAI.PartitionPilot.Forcing.PosetAction.act line 151
  15. theorem OAI.PartitionPilot.Forcing.PosetAction.act_one line 153
  16. theorem OAI.PartitionPilot.Forcing.PosetAction.act_mul line 158
  17. theorem OAI.PartitionPilot.Forcing.PosetAction.act_inv_left line 166
  18. theorem OAI.PartitionPilot.Forcing.PosetAction.act_inv_right line 169
  19. def OAI.PartitionPilot.Forcing.PosetAction.nameEquiv line 172
  20. theorem OAI.PartitionPilot.Forcing.PosetAction.entry_act line 178
  21. theorem OAI.PartitionPilot.Forcing.PosetAction.eval_act line 190
  22. theorem OAI.PartitionPilot.Forcing.PosetAction.act_check line 194
  23. def OAI.PartitionPilot.Forcing.PosetAction.stabilizer line 198
  24. theorem OAI.PartitionPilot.Forcing.PosetAction.stabilizer_conjugation line 211
  25. def OAI.PartitionPilot.Forcing.PosetAction.pullbackFilter line 230
  26. theorem OAI.PartitionPilot.Forcing.PosetAction.forcesEq_act line 255
  27. theorem OAI.PartitionPilot.Forcing.PosetAction.forcesEq_act_iff line 280
  28. theorem OAI.PartitionPilot.Forcing.PosetAction.forcesMem_act line 289
  29. theorem OAI.PartitionPilot.Forcing.PosetAction.forcesMem_act_iff line 298
  30. theorem OAI.PartitionPilot.Forcing.PosetAction.act_rename_of_equivariant line 322
  31. theorem OAI.PartitionPilot.Forcing.PosetAction.stabilizer_le_rename line 331
  32. theorem OAI.PartitionPilot.Forcing.PosetAction.support_le_rename line 338
  33. theorem OAI.PartitionPilot.Forcing.PosetAction.act_eq_of_support_agreement line 354
  34. inductive OAI.PartitionPilot.Forcing.HereditarilySymmetric line 377
  35. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.symmetric line 386
  36. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.member line 391
  37. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.translated line 396
  38. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.assemble line 408
  39. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.assemble_common line 417
  40. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.check line 432
  41. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.singleton line 441
  42. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.unorderedPair line 446
  43. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.orderedPair line 457
  44. theorem OAI.PartitionPilot.Forcing.Name.NameDomain.empty_mem line 474
  45. theorem OAI.PartitionPilot.Forcing.Name.NameDomain.empty_value_mem line 496
  46. theorem OAI.PartitionPilot.Forcing.PosetAction.empty_hs line 508
  47. theorem OAI.PartitionPilot.Forcing.SetFormula.realize_emptySet line 524
  48. theorem OAI.PartitionPilot.Forcing.HereditarilySymmetric.rename line 547
  49. theorem OAI.PartitionPilot.Compression.RecursiveMaps.NormalSubgroupFamily.fin_iInf line 566
  50. def OAI.PartitionPilot.Forcing.Name.orbitPairGraph line 596
  51. theorem OAI.PartitionPilot.Forcing.Name.entry_orbitPairGraph line 599
  52. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_orbitPairGraph line 605
  53. theorem OAI.PartitionPilot.Forcing.Name.act_pair line 619
  54. theorem OAI.PartitionPilot.Forcing.Name.act_orbitPairGraph line 625
  55. theorem OAI.PartitionPilot.Forcing.Name.orbitPairGraph_hs line 643
  56. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_left line 666
  57. theorem OAI.PartitionPilot.Forcing.TransitiveGround.pair_right line 669
  58. def OAI.PartitionPilot.Forcing.TransitiveGround.nameDomain line 672
  59. theorem OAI.PartitionPilot.Forcing.TransitiveGround.mem_nameDomain line 676
  60. theorem OAI.PartitionPilot.Forcing.TransitiveGround.empty_mem line 678
  61. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nameDomain_nonempty line 696
  62. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nameDomain_countable line 699
  63. theorem OAI.PartitionPilot.Forcing.TransitiveGround.conditions_countable line 702