OAI/SetTheory/PartitionPrinciple/Definability/LeastSlotOwnerCodes.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.LeastSupportCode line 11
  2. def OAI.PartitionPilot.Forcing.leastSupportGraph line 15
  3. theorem OAI.PartitionPilot.Forcing.pair_mem_leastSupportGraph line 19
  4. def OAI.PartitionPilot.Forcing.BoundedFormula.leastSupportFormula line 31
  5. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_leastSupportFormula line 38
  6. def OAI.PartitionPilot.Forcing.BoundedFormula.leastSupportEntryFormula line 44
  7. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_leastSupportEntryFormula line 48
  8. theorem OAI.PartitionPilot.Forcing.TransitiveGround.leastSupportGraph_mem line 57
  9. theorem OAI.PartitionPilot.Forcing.leastSupportCode_iff line 85
  10. theorem OAI.PartitionPilot.Forcing.leastSupportGraph_entry line 108
  11. theorem OAI.PartitionPilot.Forcing.leastSupportGraph_function line 114
  12. def OAI.PartitionPilot.Forcing.LeastSlotCode line 135
  13. theorem OAI.PartitionPilot.Forcing.LeastSlotCode.le line 139
  14. theorem OAI.PartitionPilot.Forcing.LeastSlotCode.unique line 149
  15. theorem OAI.PartitionPilot.Forcing.exists_leastSlotCode line 156
  16. def OAI.PartitionPilot.Forcing.leastSlotOwnerGraph line 170
  17. theorem OAI.PartitionPilot.Forcing.pair_mem_leastSlotOwnerGraph line 175
  18. theorem OAI.PartitionPilot.Forcing.pair_mem_leastSlotOwnerGraph_of_owner line 187
  19. theorem OAI.PartitionPilot.Forcing.leastSlotOwnerGraph_partial line 200
  20. theorem OAI.PartitionPilot.Forcing.leastSlotOwnerGraph_function line 209
  21. theorem OAI.PartitionPilot.Forcing.leastSlotOwnerGraph_monotone line 230