OAI/Analysis/CharacterCriterion/InductiveLimit.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.KirchbergRordam.StarCompletion.star_coe line 39
  2. instance OAI.KirchbergRordam.StarCompletion.completionNormedStarGroup line 43
  3. lemma OAI.KirchbergRordam.CStarInductiveLimit.rawOf_map line 65
  4. lemma OAI.KirchbergRordam.CStarInductiveLimit.normLift_mk line 69
  5. theorem OAI.KirchbergRordam.CStarInductiveLimit.norm_rawOf line 73
  6. def OAI.KirchbergRordam.CStarInductiveLimit.rawInclusion line 77
  7. def OAI.KirchbergRordam.CStarInductiveLimit.of line 82
  8. theorem OAI.KirchbergRordam.CStarInductiveLimit.of_map line 85
  9. theorem OAI.KirchbergRordam.CStarInductiveLimit.norm_of line 91
  10. theorem OAI.KirchbergRordam.CStarInductiveLimit.of_isometry line 94
  11. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 98) line 98
  12. def OAI.KirchbergRordam.CStarInductiveLimit.rawLift line 104
  13. theorem OAI.KirchbergRordam.CStarInductiveLimit.rawLift_of line 113
  14. theorem OAI.KirchbergRordam.CStarInductiveLimit.norm_rawLift_le line 117
  15. theorem OAI.KirchbergRordam.CStarInductiveLimit.continuous_rawLift line 124
  16. def OAI.KirchbergRordam.CStarInductiveLimit.lift line 133
  17. theorem OAI.KirchbergRordam.CStarInductiveLimit.lift_rawInclusion line 157
  18. theorem OAI.KirchbergRordam.CStarInductiveLimit.lift_of line 163
  19. theorem OAI.KirchbergRordam.CStarInductiveLimit.induction_on line 170
  20. theorem OAI.KirchbergRordam.CStarInductiveLimit.hom_ext line 179
  21. theorem OAI.KirchbergRordam.CStarInductiveLimit.denseRange_of line 184
  22. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 191) line 191
  23. lemma OAI.KirchbergRordam.CStarInductiveLimit.Chain.map_self line 203
  24. lemma OAI.KirchbergRordam.CStarInductiveLimit.Chain.map_succ line 206
  25. lemma OAI.KirchbergRordam.CStarInductiveLimit.Chain.map_map line 211
  26. lemma OAI.KirchbergRordam.CStarInductiveLimit.Chain.norm_map line 219