OAI/Computability/DegreeRigidity/CohenForcing/ForcingProjection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.TuringRigidity.ForcingProjection.Projection line 10
  2. def OAI.TuringRigidity.ForcingProjection.imageFilter line 15
  3. def OAI.TuringRigidity.ForcingProjection.pullDense line 24
  4. theorem OAI.TuringRigidity.ForcingProjection.pullDense_dense line 27
  5. theorem OAI.TuringRigidity.ForcingProjection.image_meets line 34
  6. theorem OAI.TuringRigidity.ForcingProjection.image_generic line 40
  7. def OAI.TuringRigidity.ForcingProjection.QuotientConditions line 44
  8. instance OAI.TuringRigidity.ForcingProjection.quotientPreorder line 47
  9. def OAI.TuringRigidity.ForcingProjection.quotientFilter line 50
  10. def OAI.TuringRigidity.ForcingProjection.liftFilter line 62
  11. theorem OAI.TuringRigidity.ForcingProjection.lift_mem_iff line 72
  12. theorem OAI.TuringRigidity.ForcingProjection.lift_quotient_eq line 77
  13. theorem OAI.TuringRigidity.ForcingProjection.image_lift_subset line 82
  14. def OAI.TuringRigidity.ForcingProjection.projectionCone line 88
  15. theorem OAI.TuringRigidity.ForcingProjection.projectionCone_dense line 91
  16. theorem OAI.TuringRigidity.ForcingProjection.image_lift_eq line 100