OAI/Analysis/KadisonKastler/NormUltraproductMaps.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinate embeddings induce faithful norm-ultraproduct embeddings

  1. def OAI.KadisonKastler.normProductMap line 18
  2. theorem OAI.KadisonKastler.normProductMap_apply line 29
  3. theorem OAI.KadisonKastler.NormNullSequence.map line 32
  4. def OAI.KadisonKastler.normUltraproductInducedMap line 37
  5. theorem OAI.KadisonKastler.normUltraproductInducedMap_apply_map line 44
  6. theorem OAI.KadisonKastler.normUltraproductInducedMap_injective line 50