OAI/Analysis/KadisonKastler/StarEquivProjectionLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Projection suprema and normality of an algebraic star isomorphism

The order isomorphism preserves directed projection suprema. Their concrete vector limits therefore also hold in the target faithful representation.

  1. def OAI.KadisonKastler.algebraProjectionOrderIso line 23
  2. theorem OAI.KadisonKastler.starEquiv_projection_isLUB line 39
  3. theorem OAI.KadisonKastler.starEquiv_projection_vector_tendsto line 49
  4. theorem OAI.KadisonKastler.starEquiv_projection_strong_tendsto line 59