OAI/Computability/DegreeRigidity/Representation/CommonIdealSelection.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.CommonIdeal.even line 9
  2. def OAI.TuringRigidity.CommonIdeal.odd line 10
  3. def OAI.TuringRigidity.CommonIdeal.pad line 11
  4. theorem OAI.TuringRigidity.CommonIdeal.pad_extends line 13
  5. theorem OAI.TuringRigidity.CommonIdeal.extends_of_prefix line 15
  6. theorem OAI.TuringRigidity.CommonIdeal.join_columns line 22
  7. def OAI.TuringRigidity.CommonIdeal.Embeds line 33
  8. theorem OAI.TuringRigidity.CommonIdeal.embeds_initialWord line 36
  9. theorem OAI.TuringRigidity.CommonIdeal.join_extends_input line 50
  10. def OAI.TuringRigidity.CommonIdeal.family line 69
  11. theorem OAI.TuringRigidity.CommonIdeal.family_dense line 73
  12. theorem OAI.TuringRigidity.CommonIdeal.family_measurable line 94
  13. theorem OAI.TuringRigidity.CommonIdeal.family_mono line 105
  14. theorem OAI.TuringRigidity.CommonIdeal.ideal_of_family line 111
  15. theorem OAI.TuringRigidity.CommonIdeal.borel_selected_common_ideal line 124
  16. theorem OAI.TuringRigidity.CommonIdeal.borel_selected_common_ideal_with line 139