OAI/Analysis/KadisonKastler/RealNestCompletion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous contractive completion along a real-indexed nest

Finite chains are completed explicitly. A bounded weak operator limit over finite subsets imposes all the prescribed lower corners at once.

  1. theorem OAI.KadisonKastler.finite_real_nest_completion line 22
  2. theorem OAI.KadisonKastler.real_nest_contractive_completion line 42