OAI/Analysis/PureInfiniteness/FiniteOneStepReduction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite part of KR02 Proposition 7.14: an approximation by finitely many inner coefficients collapses to one whenever the targets commute.

  1. theorem OAI.WeakPureInfiniteness.finite_oneStep_reduction line 21