OAI/SetTheory/PartitionPrinciple/Definability/NonemptyTupleFields.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartitionPilot.Forcing.nonemptyTupleCode line 10
  2. theorem OAI.PartitionPilot.Forcing.nonemptyTupleCode_injective line 14
  3. def OAI.PartitionPilot.Forcing.BoundedFormula.nonemptyTupleFormula line 31
  4. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_nonemptyTupleFormula line 38
  5. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nonemptyTupleCode_mem line 66
  6. theorem OAI.PartitionPilot.Forcing.TransitiveGround.nonemptyTupleCode_field_mem line 73
  7. def OAI.PartitionPilot.Forcing.BoundedFormula.reindex line 95
  8. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_reindex line 102
  9. def OAI.PartitionPilot.Forcing.BoundedFormula.exPairFields line 118
  10. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_exPairFields line 123
  11. def OAI.PartitionPilot.Forcing.BoundedFormula.tupleShapeFormula line 147
  12. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_tupleShapeFormula line 151
  13. def OAI.PartitionPilot.Forcing.refinementIndexCode line 176
  14. theorem OAI.PartitionPilot.Forcing.refinementIndexCode_eq_iff line 179
  15. def OAI.PartitionPilot.Forcing.refinementIndexBound line 185
  16. theorem OAI.PartitionPilot.Forcing.mem_refinementIndexBound line 188
  17. theorem OAI.PartitionPilot.Forcing.refinementIndexCode_mem_bound line 201
  18. def OAI.PartitionPilot.Forcing.BoundedFormula.refinementIndexFormula line 214
  19. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_refinementIndexFormula line 217
  20. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexCode_mem line 235
  21. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexCode_fields_mem line 243
  22. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexBound_mem line 250
  23. def OAI.PartitionPilot.Forcing.refinementIndexFieldGraph line 269
  24. theorem OAI.PartitionPilot.Forcing.pair_mem_refinementIndexFieldGraph line 274
  25. theorem OAI.PartitionPilot.Forcing.refinementIndexFieldGraph_entry line 284
  26. theorem OAI.PartitionPilot.Forcing.refinementIndexFieldGraph_function line 296
  27. def OAI.PartitionPilot.Forcing.SetFormula.refinementIndexFieldFormula line 308
  28. theorem OAI.PartitionPilot.Forcing.TransitiveGround.realize_refinementIndexFieldFormula line 320
  29. theorem OAI.PartitionPilot.Forcing.TransitiveGround.refinementIndexFieldGraph_mem line 348
  30. theorem OAI.PartitionPilot.Forcing.TransitiveGround.graphRestriction_mem line 382
  31. theorem OAI.PartitionPilot.Forcing.TransitiveGround.functionGraphOn_ground_range line 389
  32. def OAI.PartitionPilot.Forcing.tupleFieldBound line 404
  33. theorem OAI.PartitionPilot.Forcing.nonemptyTupleCode_field_mem_bound line 408
  34. def OAI.PartitionPilot.Forcing.BoundedFormula.tupleFieldFormula line 419
  35. theorem OAI.PartitionPilot.Forcing.BoundedFormula.truth_tupleFieldFormula line 425
  36. theorem OAI.PartitionPilot.Forcing.TransitiveGround.tupleFieldBound_mem line 468