OAI/Analysis/JiangSu/DimensionDrop/SequentialLimitSimplicity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SequentialCStar.selfAdjoint_span_star line 16
  2. def OAI.SequentialCStar.generatedClosedStarIdeal line 30
  3. lemma OAI.SequentialCStar.generatedClosedStarIdeal_mem line 40
  4. lemma OAI.SequentialCStar.generatedClosedStarIdeal_le line 46
  5. def OAI.SequentialCStar.System.EventuallyFull line 58
  6. lemma OAI.SequentialCStar.System.closedStarIdeal_trivial line 63
  7. theorem OAI.SequentialCStar.System.limit_topologicallySimple line 115
  8. lemma OAI.OriginalJiangSu.system_eventuallyFull line 146
  9. theorem OAI.OriginalJiangSu.simple line 153