OAI/Analysis/KadisonKastler/PolarCommutantDuality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The reverse polar-commutant inclusion

The vector-state identity and the inclusion of the conjugated commutant into M already force the reverse inclusion. Density upgrades the vector identity to operator commutation. This is the last algebraic step in the modular proof.

  1. theorem OAI.KadisonKastler.polar_commutant_reverse line 20