OAI/Computability/DegreeRigidity/Syntax/BooleanProjection.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.BooleanProjection.project line 13
  2. theorem OAI.TuringRigidity.BooleanProjection.project_mem line 16
  3. theorem OAI.TuringRigidity.BooleanProjection.le_project line 19
  4. theorem OAI.TuringRigidity.BooleanProjection.project_le_iff line 22
  5. theorem OAI.TuringRigidity.BooleanProjection.project_fixed line 26
  6. theorem OAI.TuringRigidity.BooleanProjection.project_mono line 30
  7. theorem OAI.TuringRigidity.BooleanProjection.project_bot line 34
  8. theorem OAI.TuringRigidity.BooleanProjection.project_nonzero line 37
  9. theorem OAI.TuringRigidity.BooleanProjection.project_inf line 42
  10. def OAI.TuringRigidity.BooleanProjection.Positive line 59
  11. instance OAI.TuringRigidity.BooleanProjection.positiveOrder line 61
  12. def OAI.TuringRigidity.BooleanProjection.PartPositive line 64
  13. instance OAI.TuringRigidity.BooleanProjection.partPositiveOrder line 66
  14. def OAI.TuringRigidity.BooleanProjection.forcingProjection line 69
  15. theorem OAI.TuringRigidity.BooleanProjection.forcingProjection_exact line 82
  16. theorem OAI.TuringRigidity.BooleanProjection.projected_dense line 94
  17. theorem OAI.TuringRigidity.BooleanProjection.projected_countable_dense line 102