FiniteTensorApproximation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite elementary sums approximating an element of the minimal tensor product, in the form needed by simultaneous pure-state excision.

theorem OAI.WeakPureInfiniteness.exists_finite_tensor_approximation line 17