CommonMatrixPreparation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Preparing a common infinite matrix algebra

The actual countable matrix units lie in the injective algebra generated by factorial matrix stages. Moving that algebra into the neighbor makes the ordinary gap control every matrix size, with no linear selection of approximants.

theorem OAI.KadisonKastler.exists_common_matrix_preparation line 26
Source documentation
One small correction makes the given countable matrix units common and upgrades the original metric gap to two-sided matrix proximity.
```
theorem exists_common_matrix_preparation
    (hAFD : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity
theorem OAI.KadisonKastler.exists_typeIII_matrix_preparation line 52
Source documentation
In a type III factor, the published projection comparison supplies the countable matrix units required by the preceding preparation theorem.
```
theorem exists_typeIII_matrix_preparation
    (hCompare : PublishedTypeIIIProjectionComparison.{u})
    (hAFD : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity