OAI/Analysis/KadisonKastler/RelativeProjectionInsertion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Inserting a bicentralizer projection cut into a larger matrix stage

The fixed residual gap survives exact containment of the chosen projection. The reference displacement can be made arbitrarily small.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_relative_projection_insertion line 24