OAI/Analysis/KadisonKastler/InjectivityTransport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transport of an ambient contractive projection

An isomorphism of represented algebras transports injectivity whenever it extends to a contractive linear map of the ambient operator spaces. The application uses compression of a countable diagonal amplification.

  1. theorem OAI.KadisonKastler.isInjective_of_contracting_extension line 22