OAI/Analysis/KadisonKastler/NormClosureUnitBall.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unit balls and norm closure of a star subalgebra

Radial rescaling of a norm approximant preserves algebra membership and costs at most a second copy of the approximation error.

  1. theorem OAI.KadisonKastler.normClosure_unitBall_approx line 19