OAI/Analysis/Commutator/CountableProjectionJoin.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.ProjectionJoin.finiteJoin line 22
  2. lemma OAI.Kadison.ProjectionJoin.finiteJoin_projection line 26
  3. lemma OAI.Kadison.ProjectionJoin.finiteJoin_mem line 31
  4. lemma OAI.Kadison.ProjectionJoin.finiteJoin_mono line 37
  5. lemma OAI.Kadison.ProjectionJoin.le_finiteJoin_succ line 40
  6. lemma OAI.Kadison.ProjectionJoin.finiteJoin_le line 43
  7. theorem OAI.Kadison.ProjectionJoin.exists_countable_sup line 49
  8. def OAI.Kadison.ProjectionJoin.sup line 59
  9. lemma OAI.Kadison.ProjectionJoin.sup_mem line 63
  10. lemma OAI.Kadison.ProjectionJoin.sup_projection line 67
  11. lemma OAI.Kadison.ProjectionJoin.le_sup line 71
  12. lemma OAI.Kadison.ProjectionJoin.sup_strong line 75
  13. lemma OAI.Kadison.ProjectionJoin.sup_le line 80
  14. lemma OAI.Kadison.ProjectionJoin.dimension_finiteJoin_le line 95
  15. theorem OAI.Kadison.ProjectionJoin.dimension_sup_le line 105