OAI/Computability/DegreeRigidity/CohenForcing/CountableForcing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TuringRigidity.CountableForcing.GenericFilter line 9
  2. def OAI.TuringRigidity.CountableForcing.Dense line 15
  3. def OAI.TuringRigidity.CountableForcing.GenericFor line 17
  4. theorem OAI.TuringRigidity.CountableForcing.exists_generic line 20
  5. inductive OAI.TuringRigidity.CountableForcing.Sentence line 38
  6. def OAI.TuringRigidity.CountableForcing.Sentence.Truth line 48
  7. def OAI.TuringRigidity.CountableForcing.Sentence.Forces line 55
  8. theorem OAI.TuringRigidity.CountableForcing.Sentence.forces_mono line 62
  9. def OAI.TuringRigidity.CountableForcing.Sentence.Decision line 71
  10. theorem OAI.TuringRigidity.CountableForcing.Sentence.decision_dense line 73
  11. def OAI.TuringRigidity.CountableForcing.Sentence.Requirements line 81
  12. theorem OAI.TuringRigidity.CountableForcing.Sentence.requirements_dense line 88
  13. theorem OAI.TuringRigidity.CountableForcing.Sentence.requirements_mono line 96
  14. theorem OAI.TuringRigidity.CountableForcing.Sentence.generic_truth line 119
  15. def OAI.TuringRigidity.CountableForcing.Sentence.WeakForces line 163
  16. theorem OAI.TuringRigidity.CountableForcing.Sentence.weak_iff_all_generic line 165