OAI/Topology/CoarseAssembly/UnitalStructureAlgebra.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The unit of the controlled pseudolocal algebra

  1. theorem OAI.CoarseAssembly.DiscreteRoe.propagationLE_one line 22
  2. theorem OAI.CoarseAssembly.DiscreteRoe.structureGenerator_one line 28
  3. theorem OAI.CoarseAssembly.DiscreteRoe.structureAlgebra_one line 38
  4. def OAI.CoarseAssembly.DiscreteRoe.unitalStructureAlgebra line 43

    Source documentation

    The controlled structure algebra with its actual identity operator.

    def unitalStructureAlgebra : StarSubalgebra ℂ (Operator X H) where
…

    Mentions: OAI.CoarseAssembly.DiscreteRoe.Operator

  5. theorem OAI.CoarseAssembly.DiscreteRoe.unitalStructureAlgebra_closed line 52
  6. instance OAI.CoarseAssembly.DiscreteRoe.(instance at line 56) line 56
  7. instance OAI.CoarseAssembly.DiscreteRoe.(instance at line 59) line 59