OAI/Analysis/PureInfiniteness/UltrapowerCopiesExact.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The finite relative copies needed in KR02 Proposition 7.14. The relations are imposed on the selected commuting positive elements, which is sufficient for combining their coefficient compressions.

  1. abbrev OAI.WeakPureInfiniteness.CopyTest line 24
  2. def OAI.WeakPureInfiniteness.copyTestValue line 26
  3. lemma OAI.WeakPureInfiniteness.copyTestValue_nonneg line 37
  4. theorem OAI.WeakPureInfiniteness.ultrapower_copies_exact line 45
  5. theorem OAI.WeakPureInfiniteness.ultrapower_relative_copies line 134