OAI/SetTheory/PartitionPrinciple/Forcing/NameOrbitBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PartitionPilot.Forcing.PosetAction.separationPredicate_act line 14
  2. theorem OAI.PartitionPilot.Forcing.PosetAction.act_separationName line 33
  3. theorem OAI.PartitionPilot.Forcing.PosetAction.separationName_hs line 42
  4. def OAI.PartitionPilot.Forcing.PosetAction.symmetricDomain line 75
  5. theorem OAI.PartitionPilot.Forcing.PosetAction.symmetricDomain_translated line 79
  6. theorem OAI.PartitionPilot.Forcing.PosetAction.symmetricDomain_mix line 85
  7. theorem OAI.PartitionPilot.Forcing.PosetAction.mem_symmetric_values line 92
  8. def OAI.PartitionPilot.Forcing.Name.BoundedNames line 114
  9. instance OAI.PartitionPilot.Forcing.Name.boundedNames_small line 116
  10. def OAI.PartitionPilot.Forcing.Name.codedPower line 123
  11. theorem OAI.PartitionPilot.Forcing.Name.entry_codedPower line 126
  12. theorem OAI.PartitionPilot.Forcing.Name.mem_eval_codedPower line 135
  13. theorem OAI.PartitionPilot.Forcing.PosetAction.act_codedPower_fixed line 156
  14. theorem OAI.PartitionPilot.Forcing.PosetAction.codedPower_hs line 176
  15. theorem OAI.PartitionPilot.Forcing.PosetAction.symmetricDomain_nonempty line 206
  16. theorem OAI.PartitionPilot.Forcing.PosetAction.symmetric_values_pair line 210
  17. theorem OAI.PartitionPilot.Forcing.PosetAction.symmetric_values_union line 222
  18. theorem OAI.PartitionPilot.Forcing.PosetAction.symmetric_values_separation line 231
  19. theorem OAI.PartitionPilot.Forcing.PosetAction.symmetric_values_separation_params line 250
  20. def OAI.PartitionPilot.Forcing.PosetAction.orbitCodes line 283
  21. theorem OAI.PartitionPilot.Forcing.PosetAction.mem_orbitCodes line 286
  22. theorem OAI.PartitionPilot.Forcing.PosetAction.mem_orbitCodes_of_mem line 295
  23. theorem OAI.PartitionPilot.Forcing.PosetAction.act_mem_orbitCodes_iff line 299
  24. theorem OAI.PartitionPilot.Forcing.PosetAction.orbitCodedPower_hs line 312