OAI/Analysis/KadisonKastler/MinimalRowBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Complete norm bounds agree throughout a minimal row family.

  1. theorem OAI.KadisonKastler.minimal_row_family_complete_bound line 21