OAI/Computability/DegreeRigidity/SetModels/DenseInclusionExtension.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TuringRigidity.DenseInclusionExtension.upperSetline 9 - def
OAI.TuringRigidity.DenseInclusionExtension.restrictSetline 12 - theorem
OAI.TuringRigidity.DenseInclusionExtension.upperSet_memline 14 - theorem
OAI.TuringRigidity.DenseInclusionExtension.restrictSet_memline 21 - theorem
OAI.TuringRigidity.DenseInclusionExtension.pushFilterSet_eqline 27 - theorem
OAI.TuringRigidity.DenseInclusionExtension.originalFilterSet_eqline 44 - theorem
OAI.TuringRigidity.DenseInclusionExtension.extension_eqline 59