OAI/Algebra/Finitistic/Localization/SourceEvaluation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.SourceEvaluation.evaluation line 14
  2. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 16) line 16
  3. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 17) line 17
  4. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 18) line 18
  5. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 19) line 19
  6. def OAI.LittleFinitistic.SourceEvaluation.vertexIso line 21
  7. lemma OAI.LittleFinitistic.SourceEvaluation.arrow01_square line 26
  8. lemma OAI.LittleFinitistic.SourceEvaluation.arrow12_square line 34
  9. lemma OAI.LittleFinitistic.SourceEvaluation.actionArrow_zero line 42
  10. instance OAI.LittleFinitistic.SourceEvaluation.first_inverted line 47
  11. instance OAI.LittleFinitistic.SourceEvaluation.second_inverted line 54
  12. def OAI.LittleFinitistic.SourceEvaluation.finite line 63
  13. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 65) line 65
  14. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 66) line 66
  15. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 67) line 67
  16. instance OAI.LittleFinitistic.SourceEvaluation.finite_first line 68
  17. instance OAI.LittleFinitistic.SourceEvaluation.finite_second line 72
  18. def OAI.LittleFinitistic.SourceEvaluation.quotientFinite line 77
  19. def OAI.LittleFinitistic.SourceEvaluation.finiteFactors line 79
  20. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 81) line 81
  21. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 84) line 84
  22. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 85) line 85
  23. def OAI.LittleFinitistic.SourceEvaluation.quotientHomotopy line 87
  24. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 89) line 89
  25. def OAI.LittleFinitistic.SourceEvaluation.homotopyFactors line 91
  26. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 93) line 93
  27. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 95) line 95
  28. def OAI.LittleFinitistic.SourceEvaluation.quotientVertexIso line 99
  29. lemma OAI.LittleFinitistic.SourceEvaluation.quotient_arrow01_square line 104
  30. def OAI.LittleFinitistic.SourceEvaluation.derived line 115
  31. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 117) line 117
  32. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 118) line 118
  33. instance OAI.LittleFinitistic.SourceEvaluation.(instance at line 119) line 119
  34. def OAI.LittleFinitistic.SourceEvaluation.derivedVertexIso line 121