OAI/Analysis/Nuclearity/TensorIdealExcisionCut.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact cut step in the elementary-ideal argument. A small image of an elementary positive tensor gives an elementary tensor in the kernel.

  1. def OAI.WeakPureInfiniteness.rightEmbedding line 18
  2. theorem OAI.WeakPureInfiniteness.elementary_cut_mem_kernel line 26