OAI/Analysis/PureInfiniteness/CollapseFiniteCompression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite coefficient identity in KR02 Proposition 7.14. Relative copies of the commuting compressed coefficients turn the finite sum into one inner compression.

  1. lemma OAI.WeakPureInfiniteness.collapse_compression_of_relative_copies line 16
  2. lemma OAI.WeakPureInfiniteness.collapse_compression_error_le line 40