OAI/Computability/DegreeRigidity/Syntax/SigmaHull.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TuringRigidity.BoundedSetTheory.SigmaFormula.matrix line 11
2. def OAI.TuringRigidity.BoundedSetTheory.SigmaFormula.prefixLength line 15
3. def OAI.TuringRigidity.BoundedSetTheory.SigmaFormula.feed line 19
4. theorem OAI.TuringRigidity.BoundedSetTheory.SigmaFormula.feed_mem line 23
5. theorem OAI.TuringRigidity.BoundedSetTheory.SigmaFormula.realize_iff_prefix line 34
6. def OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.elements line 61
7. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.mem_elements line 65
8. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.elements_mem line 70
9. theorem OAI.TuringRigidity.BoundedSetTheory.FiniteTuple.internal_sigma_witness_hull line 80