OAI/Computability/PerfectCompleteness/Construction/FactoredFunctionsLemmas.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.FactoredFunctions.factoringSpace line 11
  2. theorem OAI.PerfectCompleteness.FactoredFunctions.mem_factoringSpace line 23
  3. theorem OAI.PerfectCompleteness.FactoredFunctions.mem_factoringSpace_iff_exists_factor line 26
  4. theorem OAI.PerfectCompleteness.FactoredFunctions.const_mem_factoringSpace line 42
  5. theorem OAI.PerfectCompleteness.FactoredFunctions.one_mem_factoringSpace line 47
  6. theorem OAI.PerfectCompleteness.FactoredFunctions.mul_mem_factoringSpace line 51
  7. theorem OAI.PerfectCompleteness.FactoredFunctions.coordinate_mem_factoringSpace line 58
  8. def OAI.PerfectCompleteness.FactoredFunctions.quadraticSpan line 63
  9. theorem OAI.PerfectCompleteness.FactoredFunctions.one_mem_quadraticSpan line 67
  10. theorem OAI.PerfectCompleteness.FactoredFunctions.product_mem_quadraticSpan line 71
  11. theorem OAI.PerfectCompleteness.FactoredFunctions.quadraticSpan_le_factoringSpace line 75
  12. def OAI.PerfectCompleteness.FactoredFunctions.realizer line 86
  13. theorem OAI.PerfectCompleteness.FactoredFunctions.realizer_spec line 89
  14. def OAI.PerfectCompleteness.FactoredFunctions.evaluation line 93
  15. theorem OAI.PerfectCompleteness.FactoredFunctions.evaluation_apply line 97
  16. theorem OAI.PerfectCompleteness.FactoredFunctions.evaluation_apply_of_eq line 101
  17. theorem OAI.PerfectCompleteness.FactoredFunctions.evaluation_eq_pointEvaluation line 106
  18. theorem OAI.PerfectCompleteness.FactoredFunctions.evaluation_at_image line 114
  19. theorem OAI.PerfectCompleteness.FactoredFunctions.evaluation_one line 119
  20. theorem OAI.PerfectCompleteness.FactoredFunctionsDependent.coordinate_mem_factoringSpace line 134
  21. def OAI.PerfectCompleteness.FactoredFunctionsDependent.dependentQuadraticSpan line 140
  22. theorem OAI.PerfectCompleteness.FactoredFunctionsDependent.one_mem_dependentQuadraticSpan line 145
  23. theorem OAI.PerfectCompleteness.FactoredFunctionsDependent.product_mem_dependentQuadraticSpan line 149
  24. theorem OAI.PerfectCompleteness.FactoredFunctionsDependent.dependentQuadraticSpan_le_factoringSpace line 154