OAI/Analysis/KadisonSimilarity/Tracial/NormalTracialInclusionModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A common normal model from closed trace-vector balls. This formulation applies directly to normalized finite matrix traces.

  1. theorem OAI.KadisonSimilarity.exists_tracialInclusionModel_of_trace_balls line 17