OAI/SetTheory/PartitionPrinciple/Definability/FiniteWordMapCodes.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.finiteWordGraph line 12
  2. theorem OAI.PartitionPilot.Forcing.finiteWordGraph_function line 15
  3. theorem OAI.PartitionPilot.Forcing.mem_finiteWordGraph line 19
  4. theorem OAI.PartitionPilot.Forcing.pair_mem_finiteWordGraph line 25
  5. theorem OAI.PartitionPilot.Forcing.finiteWordGraph_nil line 38
  6. theorem OAI.PartitionPilot.Forcing.exists_finiteWordGraph line 45
  7. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordGraph_mem line 77
  8. theorem OAI.PartitionPilot.Forcing.finiteWordGraph_injective line 88
  9. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordGraph_mem_finiteWords line 112
  10. theorem OAI.PartitionPilot.Forcing.TransitiveGround.finiteWords_exact_lists line 118
  11. def OAI.PartitionPilot.Forcing.TransitiveGround.finiteWordPresentation line 128
  12. def OAI.PartitionPilot.Forcing.FiniteWordMapCode line 141
  13. def OAI.PartitionPilot.Forcing.BoundedFormula.finiteWordMapFormula line 148
  14. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_finiteWordMapFormula line 156
  15. theorem OAI.PartitionPilot.Forcing.finiteWordMapCode_iff line 166