OAI/Analysis/KadisonKastler/SupportVectorTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Moving a supported vector back to the original representation

Isometries onto its left and right supports turn a vector into a separating and cyclic vector on the original Hilbert space. Only the concrete support identities enter the proof.

  1. theorem OAI.KadisonKastler.support_transfer_separating line 21
  2. theorem OAI.KadisonKastler.support_transfer_cyclic line 65