OAI/Analysis/KadisonKastler/CentralPairFromRankModel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Packaging the constructed rank model as the exact central-pair data

  1. theorem OAI.KadisonKastler.sourceInclusion_comp line 24
  2. theorem OAI.KadisonKastler.centralPairDecomposition_of_rankModel line 35