OAI/Analysis/BoundedHochschild/MinimalProjectionNorms.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every projection corner retains the norm of right compression in a minimal represented averaging family.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.minimal_family_projection_norm line 20