OAI/Computability/DegreeRigidity/SetModels/CollapseDenseWithoutChoice.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.extend_length_without_choiceline 12 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.covers_mem_without_choiceline 30 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.definedAt_mem_without_choiceline 38 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.covers_dense_without_choiceline 49 - theorem
OAI.TuringRigidity.BoundedSetTheory.InternalCollapse.definedAt_dense_without_choiceline 66