OAI/Analysis/PureInfiniteness/AbsorptionFromTensorIdeal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Absorption from local relative Cuntz pairs, the common-null tensor-ideal span property (KR02 Lemma 7.18, using Blackadar Theorem 3.3), and a connected approximate half-flip (Kirchberg 2006, Proposition 4.4 and Remark 4.6).

  1. theorem OAI.WeakPureInfiniteness.Campaign.nuclear_absorption_from_tensor_ideal_and_halfFlip line 23