OAI/Analysis/PureInfiniteness/RelativeCoefficientEnlargement.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The relative-domain coefficient and closure step of KR02 Lemma 7.20. Domain coefficients lie in the nuclear subalgebra; implementing coefficients lie in the ambient ultrapower.

  1. def OAI.WeakPureInfiniteness.relativeCoefficientEnlargement line 17
  2. lemma OAI.WeakPureInfiniteness.relativeCoefficientEnlargement_inner line 20
  3. lemma OAI.WeakPureInfiniteness.relativeCoefficientEnlargement_error_le line 28
  4. lemma OAI.WeakPureInfiniteness.ApproximatelyOneStepAlong.coefficientEnlargement line 60