OAI/Analysis/KadisonKastler/FiniteMatrixUltraproductConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The required growing finite-matrix tracial ultraproduct

  1. def OAI.KadisonKastler.constructedFiniteMatrixUltraproduct line 19
  2. theorem OAI.KadisonKastler.publishedFiniteMatrixUltraproduct line 33

    Source documentation

    Popa §1.6 for the precise finite-matrix sequence used in the application.

    theorem publishedFiniteMatrixUltraproduct : PublishedFiniteMatrixUltraproduct := by
…

    Mentions: OAI.KadisonKastler.PublishedFiniteMatrixUltraproduct