OAI/Computability/DegreeRigidity/SetModels/RegularDecisionPartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.RegularDecisionPartition.meet line 9
2. theorem OAI.TuringRigidity.RegularDecisionPartition.meet_mem line 11
3. theorem OAI.TuringRigidity.RegularDecisionPartition.meet_isCode line 17
4. theorem OAI.TuringRigidity.RegularDecisionPartition.disjoint_le_neg line 25
5. theorem OAI.TuringRigidity.RegularDecisionPartition.remainder_empty_le line 33
6. def OAI.TuringRigidity.RegularDecisionPartition.Refines line 46
7. def OAI.TuringRigidity.RegularDecisionPartition.decidesFormula line 49
8. theorem OAI.TuringRigidity.RegularDecisionPartition.decidesFormula_spec line 53
9. def OAI.TuringRigidity.RegularDecisionPartition.refiningFormula line 61
10. theorem OAI.TuringRigidity.RegularDecisionPartition.refiningFormula_spec line 64
11. theorem OAI.TuringRigidity.RegularDecisionPartition.refining_partition line 68