OAI/Analysis/KadisonKastler/ProperInfiniteMatrixPreparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Matrix preparation for a properly infinite identity

  1. theorem OAI.KadisonKastler.exists_properInfinite_matrix_preparation line 21

    Source documentation

    Countable copies of the identity yield the infinite matrix corner needed by the common-matrix preparation.

    theorem exists_properInfinite_matrix_preparation
    (hCopies : PublishedProperInfiniteProjectionCopies.{u})
    (hAFD : PublishedIncreasingMatrixInjectivity (H := H))
…

    Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity