OAI/Analysis/FiniteFactor/CrossedProduct/FiniteAlgebra.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.sourceAlgebra_finite line 10

   Source documentation

   The actual generated source algebra is finite: every isometry is unitary.

   theorem sourceAlgebra_finite (θ : SourceCoordinate → ℝ) : IsFiniteAlgebra (sourceAlgebra θ) := by
   …

   Mentions: OAI.FiniteFactor.SourceCoordinate, OAI.FiniteFactor.IsFiniteAlgebra, OAI.FiniteFactor.sourceAlgebra