OAI/Analysis/Commutator/KaplanskyRational.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.Kaplansky.rationalClip line 15
  2. def OAI.Kadison.Kaplansky.rationalKernel line 17
  3. lemma OAI.Kadison.Kaplansky.denom_pos line 19
  4. lemma OAI.Kadison.Kaplansky.continuous_rationalKernel line 21
  5. lemma OAI.Kadison.Kaplansky.continuous_rationalClip line 25
  6. lemma OAI.Kadison.Kaplansky.rationalKernel_bound line 30
  7. lemma OAI.Kadison.Kaplansky.rationalClip_bound line 34
  8. def OAI.Kadison.Kaplansky.rationalLift line 40
  9. lemma OAI.Kadison.Kaplansky.lift_denom_pos line 42
  10. lemma OAI.Kadison.Kaplansky.continuous_rationalLift line 44
  11. lemma OAI.Kadison.Kaplansky.rationalClip_lift line 50
  12. def OAI.Kadison.Kaplansky.kernel line 66
  13. def OAI.Kadison.Kaplansky.clip line 68
  14. lemma OAI.Kadison.Kaplansky.kernel_norm_le line 70
  15. lemma OAI.Kadison.Kaplansky.clip_norm_le line 73
  16. lemma OAI.Kadison.Kaplansky.clip_selfAdjoint line 76
  17. lemma OAI.Kadison.Kaplansky.kernel_selfAdjoint line 78
  18. lemma OAI.Kadison.Kaplansky.clip_formula line 80
  19. lemma OAI.Kadison.Kaplansky.kernel_commute line 91
  20. lemma OAI.Kadison.Kaplansky.kernel_den line 95
  21. lemma OAI.Kadison.Kaplansky.den_kernel line 106
  22. lemma OAI.Kadison.Kaplansky.clip_difference line 110
  23. def OAI.Kadison.Kaplansky.lift line 124
  24. lemma OAI.Kadison.Kaplansky.lift_selfAdjoint line 126
  25. lemma OAI.Kadison.Kaplansky.clip_lift line 128