OAI/Analysis/KadisonKastler/ConstructedMatrixPositionStability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-factor stability with the common tracial position constructed

  1. theorem OAI.KadisonKastler.constructed_common_matrix_subfactor_spatial_stability line 20
  2. theorem OAI.KadisonKastler.constructed_finiteFactor_spatial_of_matrixStages_and_boundary line 61