OAI/Computability/DegreeRigidity/Effective/IndependentFamily.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.IndependentFamily.fresh line 8
  2. theorem OAI.TuringRigidity.IndependentFamily.fresh_spec line 11
  3. def OAI.TuringRigidity.IndependentFamily.tower line 15
  4. def OAI.TuringRigidity.IndependentFamily.column line 19
  5. theorem OAI.TuringRigidity.IndependentFamily.tower_mono line 21
  6. theorem OAI.TuringRigidity.IndependentFamily.base_le line 26
  7. theorem OAI.TuringRigidity.IndependentFamily.column_le line 28
  8. theorem OAI.TuringRigidity.IndependentFamily.finite_le line 31
  9. theorem OAI.TuringRigidity.IndependentFamily.finite_conservative line 37
  10. theorem OAI.TuringRigidity.IndependentFamily.column_membership line 66
  11. theorem OAI.TuringRigidity.IndependentFamily.independence line 102
  12. theorem OAI.TuringRigidity.IndependentFamily.column_injective line 120