OAI/Analysis/Nuclearity/UnitizedFiniteCoefficientCone.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite sums in the coefficient cone, allowing output coefficients in the unitization. The local relative copies still give implementing elements in the original algebra.

  1. lemma OAI.WeakPureInfiniteness.merged_unitized_coefficient_identity line 18
  2. theorem OAI.WeakPureInfiniteness.approximately_oneStepAlong_unitized_finite_coefficient_sum line 52