OAI/Analysis/KadisonKastler/CloseProjectionConjugacy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A controlled unitary conjugating two close projections

The construction takes place inside the chosen C-star algebra. Applying it to a relative commutant therefore preserves the common subalgebra.

  1. theorem OAI.KadisonKastler.polar_unitary_intertwines_selfAdjoint line 18
  2. theorem OAI.KadisonKastler.exists_unitary_conjugating_close_projections line 45