OAI/Analysis/Nuclearity/UnitizedCoefficientConvexity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Convexity of the actual finite coefficient cone. Padding arrays by zero allows unrelated finite coefficient sizes to be combined without changing their maps.

  1. lemma OAI.WeakPureInfiniteness.finiteUnitizedAbelianCoefficientCone_add line 20
  2. lemma OAI.WeakPureInfiniteness.finiteUnitizedAbelianCoefficientCone_smul line 53
  3. lemma OAI.WeakPureInfiniteness.finiteUnitizedAbelianCoefficientCone_zero line 63
  4. def OAI.WeakPureInfiniteness.unitizedCoefficientCone line 70