OAI/Analysis/PureInfiniteness/AbsorptionMain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Corollary 1.3: every separable nuclear weakly purely infinite C*-algebra absorbs O∞, without unitality or simplicity hypotheses. The fixed integer amplification condition is exactly that of the manuscript.

  1. theorem OAI.WeakPureInfiniteness.Campaign.nuclear_absorption line 17
  2. theorem OAI.WeakPureInfiniteness.Campaign.nuclear_weaklyPurelyInfinite_absorption line 23