OAI/Analysis/KadisonKastler/CornerHomogeneityTransfer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transferring a norm comparison back into a projection corner

The transfer loses no norm: a unitary comparison of the pulled-back functionals is exactly the comparison of the corresponding corner functionals. Existence of the comparison unitary is a separate theorem.

  1. theorem OAI.KadisonKastler.corner_unitary_comparison_norm line 18