OAI/Analysis/FiniteFactor/CrossedProduct/FiberSeparable.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.FiniteFactor.sourceFiber_separable line 11

   Source documentation

   Separability of the actual l2(Z) fiber, from its countable coordinate basis.

   instance sourceFiber_separable : TopologicalSpace.SeparableSpace SourceFiberHilbert := by
   …

   Mentions: OAI.FiniteFactor.SourceFiberHilbert