OAI/Analysis/Nuclearity/ConeIdealGeneration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The precise common-null ideal in KR02 Lemma 7.18 inherits elementary span from closed tensor-ideal generation. This is a structural bridge, not an assumption that nuclearity has already supplied ideal generation.

  1. theorem OAI.WeakPureInfiniteness.common_null_elementary_span_of_generation line 19
  2. theorem OAI.WeakPureInfiniteness.FunctionalTensorRepresentation.elementarySpan_of_ideal_generation line 50