OAI/SetTheory/PartitionPrinciple/Definability/TaskCapFamilyCodes.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.BoundedFormula.codedInsertionProfileFormula line 9
  2. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_codedInsertionProfileFormula line 17
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.codedCapProfileFormula line 25
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_codedCapProfileFormula line 32
  5. def OAI.PartitionPilot.Forcing.BoundedFormula.imageProfilePositiveFormula line 46
  6. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_imageProfilePositiveFormula line 50
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.imageInsertionProfileFormula line 62
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_imageInsertionProfileFormula line 70
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.imageCapProfileFormula line 79
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_imageCapProfileFormula line 86
  11. def OAI.PartitionPilot.Forcing.OldProfilePreservationCode line 110
  12. def OAI.PartitionPilot.Forcing.BoundedFormula.oldProfilePreservationFormula line 120
  13. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_oldProfilePreservationFormula line 132
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_oldProfilePreservationFormula line 141
  15. theorem OAI.PartitionPilot.Forcing.oldProfilePreservation_groundPower_iff line 152
  16. def OAI.PartitionPilot.Forcing.TaskCapProfilesCode line 169
  17. def OAI.PartitionPilot.Forcing.CommonTargetCapMeetCode line 176
  18. structure OAI.PartitionPilot.Forcing.TaskCapFamilyCode line 182
  19. def OAI.PartitionPilot.Forcing.BoundedFormula.taskCapProfilesFormula line 189
  20. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_taskCapProfilesFormula line 203
  21. def OAI.PartitionPilot.Forcing.BoundedFormula.commonTargetCapMeetFormula line 212
  22. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_commonTargetCapMeetFormula line 224
  23. def OAI.PartitionPilot.Forcing.BoundedFormula.taskCapFamilyFormula line 232
  24. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_taskCapFamilyFormula line 238
  25. theorem OAI.PartitionPilot.Forcing.BoundedFormula.realize_taskCapFamilyFormula line 247