OAI/Analysis/Nuclearity/DensePositiveExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positivity of a continuous linear map can be checked on squares in a dense range. The proof is independent of the concrete tensor completion.

  1. lemma OAI.WeakPureInfiniteness.continuousLinearMap_nonneg_of_dense_squares line 15