OAI/Analysis/KadisonKastler/NestCornerExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Extending a contractive corner across one nest projection

  1. theorem OAI.KadisonKastler.extend_contractive_nest_corner line 14