OAI/Computability/DegreeRigidity/CohenForcing/CohenNiceNames.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TuringRigidity.CohenNiceNames.compatible_symm line 11
2. theorem OAI.TuringRigidity.CohenNiceNames.compatible_refl line 14
3. theorem OAI.TuringRigidity.CohenNiceNames.countable_predense_antichain line 17
4. def OAI.TuringRigidity.CohenNiceNames.RealName line 46
5. def OAI.TuringRigidity.CohenNiceNames.value line 48
6. def OAI.TuringRigidity.CohenNiceNames.below line 51
7. def OAI.TuringRigidity.CohenNiceNames.decision line 54
8. theorem OAI.TuringRigidity.CohenNiceNames.decision_dense line 57
9. theorem OAI.TuringRigidity.CohenNiceNames.value_eq_of_generic line 69
10. theorem OAI.TuringRigidity.CohenNiceNames.countably_supported_name line 84