OAI/Analysis/WeakInfiniteness/SmallCStar.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPureInfiniteness.small_of_separable_metric line 26
  2. def OAI.WeakPureInfiniteness.SmallCStarCarrier line 35
  3. def OAI.WeakPureInfiniteness.smallCStarEquiv line 41
  4. instance OAI.WeakPureInfiniteness.smallCStarNormedRing line 43
  5. instance OAI.WeakPureInfiniteness.smallCStarAlgebraStruct line 45
  6. instance OAI.WeakPureInfiniteness.smallCStarNormedSpace line 47
  7. instance OAI.WeakPureInfiniteness.smallCStarStarRing line 50
  8. instance OAI.WeakPureInfiniteness.smallCStarStarModule line 52
  9. lemma OAI.WeakPureInfiniteness.smallCStarEquiv_isometry line 54
  10. instance OAI.WeakPureInfiniteness.smallCStarComplete line 58
  11. instance OAI.WeakPureInfiniteness.smallCStarCStar line 62
  12. def OAI.WeakPureInfiniteness.smallCStarStarAlgEquiv line 76