OAI/Analysis/Naimark/DirectLimit.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. class OAI.NaimarkZFC.IsometricStarSystem line 16
  2. instance OAI.NaimarkZFC.directLimitNorm line 21
  3. theorem OAI.NaimarkZFC.directLimit_norm_mk line 31
  4. theorem OAI.NaimarkZFC.directLimitNormCore line 34
  5. instance OAI.NaimarkZFC.directLimitNormedAddCommGroup line 53
  6. instance OAI.NaimarkZFC.directLimitNormedRing line 56
  7. instance OAI.NaimarkZFC.directLimitNormedAlgebra line 63
  8. instance OAI.NaimarkZFC.directLimitNormedStarGroup line 68
  9. instance OAI.NaimarkZFC.directLimitCStarRing line 72
  10. def OAI.NaimarkZFC.directLimitInclude line 77
  11. theorem OAI.NaimarkZFC.directLimitInclude_isometry line 86
  12. theorem OAI.NaimarkZFC.directLimitInclude_compatible line 92
  13. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 101) line 101
  14. theorem OAI.NaimarkZFC.CStarCompletion.star_coe line 104
  15. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 107) line 107
  16. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 110) line 110
  17. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 127) line 127
  18. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 134) line 134
  19. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 142) line 142
  20. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 150) line 150
  21. instance OAI.NaimarkZFC.CStarCompletion.(instance at line 153) line 153
  22. def OAI.NaimarkZFC.CStarCompletion.toCompletion line 158
  23. theorem OAI.NaimarkZFC.CStarCompletion.include_isometry line 167
  24. theorem OAI.NaimarkZFC.CStarCompletion.include_dense line 170
  25. abbrev OAI.NaimarkZFC.CStarDirectLimit line 182
  26. def OAI.NaimarkZFC.cstarDirectLimitInclude line 184
  27. theorem OAI.NaimarkZFC.cstarDirectLimitInclude_isometry line 187
  28. theorem OAI.NaimarkZFC.cstarDirectLimitInclude_compatible line 191
  29. theorem OAI.NaimarkZFC.cstarDirectLimitInclude_dense line 197
  30. theorem OAI.NaimarkZFC.cstarDirectLimit_induction line 204
  31. theorem OAI.NaimarkZFC.cstarDirectLimit_nontrivial line 213
  32. def OAI.NaimarkZFC.directLimitLift line 224
  33. theorem OAI.NaimarkZFC.directLimitLift_stage line 231
  34. def OAI.NaimarkZFC.directLimitLiftCLM line 234
  35. def OAI.NaimarkZFC.cstarDirectLimitLift line 242
  36. theorem OAI.NaimarkZFC.cstarDirectLimitLift_stage line 270
  37. theorem OAI.NaimarkZFC.cstarDirectLimitLift_isometry line 274
  38. def OAI.NaimarkZFC.cstarDirectLimitEquiv line 287