OAI/Analysis/Commutator/TriangularMetric.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.RectangularColumn.triangular_left line 33
2. lemma OAI.Kadison.RectangularColumn.triangular_right line 40
3. lemma OAI.Kadison.RectangularColumn.triangular_star_right line 46
4. abbrev OAI.Kadison.RectangularColumn.lowerFactor line 58
5. abbrev OAI.Kadison.RectangularColumn.lowerRight line 60
6. lemma OAI.Kadison.RectangularColumn.lowerFactor_right line 64
7. abbrev OAI.Kadison.RectangularColumn.metricLower line 69
8. abbrev OAI.Kadison.RectangularColumn.metricUpperRight line 71
9. lemma OAI.Kadison.RectangularColumn.metricLower_eq line 74
10. lemma OAI.Kadison.RectangularColumn.metricLower_commutes line 80
11. lemma OAI.Kadison.RectangularColumn.metricUpperRight_equation line 91
12. lemma OAI.Kadison.RectangularColumn.lowerRight_norm_le line 103
13. lemma OAI.Kadison.RectangularColumn.metricUpperRight_norm_le line 108
14. theorem OAI.Kadison.RectangularColumn.implementer_of_factor_metric line 123