OAI/Computability/DegreeRigidity/CohenForcing/CohenFilterReal.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.CohenFilterReal.Longline 9 - theorem
OAI.TuringRigidity.CohenFilterReal.long_denseline 11 - theorem
OAI.TuringRigidity.CohenFilterReal.exists_realFilterline 16 - theorem
OAI.TuringRigidity.CohenFilterReal.realFilter_longline 49 - theorem
OAI.TuringRigidity.CohenFilterReal.weak_iff_realsline 53 - theorem
OAI.TuringRigidity.CohenFilterReal.sourceEquation_weak_iff_realsline 70