OAI/Analysis/KadisonKastler/SpatialExpectedSubfactor.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two-ratio product has the required expected subfactor

Faithful-state homogeneity of the product factor transports its reference-state bicentralizer to the required faithful state.

  1. theorem OAI.KadisonKastler.PointedMatrixSites.spatial_expected_matrix_subfactor line 28