OAI/Analysis/KadisonKastler/PointedProductLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Universe lift of a concrete pointed product

The construction takes place in a separable Hilbert space in Type. Spatial transport along ULift gives the same concrete product data in any ambient universe required by the stability theorem.

  1. def OAI.KadisonKastler.PointedMatrixProduct.universeLift line 21

    Source documentation

    Raise the universe without changing any product-state data.

    def PointedMatrixProduct.universeLift {I : Type} {ν : I → ℝ}
    (P : PointedMatrixProduct.{0} ν) : PointedMatrixProduct.{u} ν := by
…