OAI/Computability/DegreeRigidity/SetModels/ModelOrderSatisfaction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BoundedSetTheory.SetAutomorphism line 10
  2. def OAI.TuringRigidity.BoundedSetTheory.Formula.setIdeal line 19
  3. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_setIdeal line 25
  4. def OAI.TuringRigidity.BoundedSetTheory.Formula.onto line 30
  5. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_onto line 32
  6. def OAI.TuringRigidity.BoundedSetTheory.Formula.surjection line 36
  7. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_surjection line 38
  8. def OAI.TuringRigidity.BoundedSetTheory.Formula.setAutomorphism line 43
  9. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.eval_setAutomorphism line 49
  10. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.realize_setIdeal line 54
  11. theorem OAI.TuringRigidity.BoundedSetTheory.Formula.realize_setAutomorphism line 59
  12. def OAI.TuringRigidity.BoundedSetTheory.LevySigma.countable line 67
  13. theorem OAI.TuringRigidity.BoundedSetTheory.LevySigma.realize_countable line 69