OAI/Analysis/KadisonKastler/TomitaComplementaryRoot.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complementary graph square root

Polar conjugation interchanges both bounded positive square roots. This expresses the full Tomita graph using its two positive coordinates.

  1. theorem OAI.KadisonKastler.conjugationOperator_nonneg line 19
  2. def OAI.KadisonKastler.tomitaGraphComplementRoot line 30
  3. theorem OAI.KadisonKastler.tomitaGraphRoot_conjugation line 33
  4. theorem OAI.KadisonKastler.tomitaGraphComplementRoot_nonneg line 43
  5. theorem OAI.KadisonKastler.tomitaGraphComplementRoot_square line 47
  6. theorem OAI.KadisonKastler.tomitaGraphRoot_polar_apply line 54
  7. theorem OAI.KadisonKastler.tomitaGraphComplementRoot_injective line 64