OAI/Computability/DegreeRigidity/OrdinalCodes/NumericDomain.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TuringRigidity.NumericSyntax.Domain line 10
  2. theorem OAI.TuringRigidity.NumericSyntax.Numeric.toDomain line 17
  3. theorem OAI.TuringRigidity.NumericSyntax.Domain.congr line 26
  4. theorem OAI.TuringRigidity.NumericSyntax.Domain.and line 30
  5. theorem OAI.TuringRigidity.NumericSyntax.Domain.neg line 35
  6. theorem OAI.TuringRigidity.NumericSyntax.Domain.imp line 39
  7. theorem OAI.TuringRigidity.NumericSyntax.Domain.subst line 42
  8. theorem OAI.TuringRigidity.NumericSyntax.Domain.existsSet line 51
  9. theorem OAI.TuringRigidity.NumericSyntax.Domain.allMem line 63
  10. theorem OAI.TuringRigidity.NumericSyntax.powerBound_domain line 77