OAI/Computability/DegreeRigidity/CohenForcing/InternalCohenFilters.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- instance
OAI.TuringRigidity.InternalCohen.cohenTopline 11 - theorem
OAI.TuringRigidity.InternalCohen.label_topline 14 - theorem
OAI.TuringRigidity.InternalCohen.conditionEquiv_topline 26 - def
OAI.TuringRigidity.InternalCohen.pullFilterline 28 - def
OAI.TuringRigidity.InternalCohen.pushFilterline 39 - theorem
OAI.TuringRigidity.InternalCohen.filter_extline 50 - theorem
OAI.TuringRigidity.InternalCohen.pull_pushline 54 - theorem
OAI.TuringRigidity.InternalCohen.push_pullline 59 - theorem
OAI.TuringRigidity.InternalCohen.dense_pull_iffline 64 - theorem
OAI.TuringRigidity.InternalCohen.groundGeneric_iffline 75 - theorem
OAI.TuringRigidity.InternalCohen.groundGeneric_longline 92 - theorem
OAI.TuringRigidity.InternalCohen.groundGeneric_realline 113