OAI/Analysis/KadisonKastler/ProjectionMatrixInsertion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inserting a projection into a finite matrix stage of a type III factor

For a nontrivial projection, its two nonzero sides are equivalent and give a two-by-two system of matrix units. The scalar projections already belong to the initial scalar stage. No state approximation is asserted.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_matrixStage_containing_projection line 23