OAI/Computability/DegreeRigidity/CohenForcing/QuotientDense.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.QuotientDense.requirementline 10 - theorem
OAI.TuringRigidity.QuotientDense.requirement_denseline 14 - def
OAI.TuringRigidity.QuotientDense.restrictionline 26 - theorem
OAI.TuringRigidity.QuotientDense.restriction_denseline 29 - theorem
OAI.TuringRigidity.QuotientDense.lift_meetsline 39 - theorem
OAI.TuringRigidity.QuotientDense.lift_genericline 46 - theorem
OAI.TuringRigidity.QuotientDense.quotient_generic_iffline 51 - theorem
OAI.TuringRigidity.QuotientDense.quotient_countableline 63