OAI/Analysis/KadisonSimilarity/Representation/SubalgebraNormality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normality of a represented subalgebra follows from closed bounded trace-vector sets, using the original ambient tracial geometry for totality.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.subalgebra_normal_range_of_closed_trace_balls line 16