OAI/Computability/DegreeRigidity/SetModels/InternalBooleanProjection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.InternalBooleanProjection.complements line 9
2. theorem OAI.TuringRigidity.InternalBooleanProjection.complements_mem line 12
3. theorem OAI.TuringRigidity.InternalBooleanProjection.inf_eq_neg_sup line 20
4. theorem OAI.TuringRigidity.InternalBooleanProjection.closed_inf line 48
5. def OAI.TuringRigidity.InternalBooleanProjection.uppers line 64
6. def OAI.TuringRigidity.InternalBooleanProjection.project line 66
7. theorem OAI.TuringRigidity.InternalBooleanProjection.uppers_mem line 68
8. theorem OAI.TuringRigidity.InternalBooleanProjection.project_internal line 74
9. theorem OAI.TuringRigidity.InternalBooleanProjection.project_mem_part line 78
10. theorem OAI.TuringRigidity.InternalBooleanProjection.subset_project line 85
11. theorem OAI.TuringRigidity.InternalBooleanProjection.project_le_iff line 88
12. theorem OAI.TuringRigidity.InternalBooleanProjection.project_fixed line 94
13. theorem OAI.TuringRigidity.InternalBooleanProjection.project_nonempty line 98