OAI/Analysis/CStarAlgebra/PureInfiniteness/ClosedIdeal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MainGap.idealWords line 12
  2. def OAI.MainGap.idealSpan line 13
  3. lemma OAI.MainGap.idealSpan_word line 15
  4. lemma OAI.MainGap.idealSpan_left line 18
  5. lemma OAI.MainGap.idealSpan_right line 27
  6. lemma OAI.MainGap.idealSpan_star line 36
  7. def OAI.MainGap.idealAlgebra line 46
  8. def OAI.MainGap.closedIdeal line 54
  9. lemma OAI.MainGap.closedIdeal_closed line 57
  10. instance OAI.MainGap.closedIdeal_complete line 60
  11. lemma OAI.MainGap.closedIdeal_word line 63
  12. lemma OAI.MainGap.self_mem_closedIdeal line 66
  13. lemma OAI.MainGap.closedIdeal_left line 69
  14. lemma OAI.MainGap.closedIdeal_right line 74