OAI/Analysis/KadisonKastler/NormalEquivOnto.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A normal representation equivalence with a specified concrete range

  1. def OAI.KadisonKastler.normalEquivOnto line 22
  2. theorem OAI.KadisonKastler.normalEquivOnto_val line 35
  3. theorem OAI.KadisonKastler.normalEquivOnto_boundedWeakNormal line 38
  4. theorem OAI.KadisonKastler.exists_normalEquivOnto line 45