OAI/Analysis/KadisonKastler/PositiveOrbitDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing distance between positive unitary orbits

The uniform contraction forces the infimum of squared orbit distances to vanish. Only the modular coisometries of the concrete product are used.

  1. theorem OAI.KadisonKastler.positive_unitary_orbit_dense line 21