OAI/Analysis/PureInfiniteness/CoefficientConeClosure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual coefficient cone and its point-norm closure are invariant under output compressions. Thus approximating the inclusion suffices for all relatively approximately inner maps, as in KR02 Lemma 7.19.

  1. lemma OAI.WeakPureInfiniteness.unitizedSandwich_output_compression line 18
  2. lemma OAI.WeakPureInfiniteness.unitizedCoefficientEnlargement_output_compression line 25
  3. def OAI.WeakPureInfiniteness.outputCompression line 32
  4. lemma OAI.WeakPureInfiniteness.outputCompression_continuous line 35
  5. lemma OAI.WeakPureInfiniteness.finiteUnitizedAbelianCoefficientCone_outputCompression line 44
  6. lemma OAI.WeakPureInfiniteness.coefficientConeClosure_outputCompression line 55
  7. theorem OAI.WeakPureInfiniteness.coefficientConeClosure_of_approximatelyInnerAlong line 62