OAI/Analysis/FiniteFactor/CrossedProduct/HilbertSeparable.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.FiniteFactor.sourceHilbert_separable line 12

   Source documentation

   The actual regular-representation Hilbert space is separable. This uses the countably generated Borel structure of the countable real product times Z and the finite exponent 2. It does not assert a predual for the algebra.

   instance sourceHilbert_separable : TopologicalSpace.SeparableSpace (SourceHilbert SourceCoordinate) := by
   …

   Mentions: OAI.FiniteFactor.SourceHilbert, OAI.FiniteFactor.SourceCoordinate