OAI/Analysis/KadisonKastler/BilateralHalfSpaces.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Closed coordinate subspaces and their constant intersection.

  1. theorem OAI.KadisonKastler.aestronglyMeasurable_of_L2_approximations line 17
  2. theorem OAI.KadisonKastler.bilateral_L2_constant_of_half_measurable line 28