OAI/Topology/CoarseAssembly/InclusionModule.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Spatial module maps for inclusions

Extension by zero along an injection is an actual Hilbert-space isometry, with the exact basis formula used for the boundary inclusions.

  1. theorem OAI.CoarseAssembly.extendedFunction_apply line 22
  2. theorem OAI.CoarseAssembly.extendedFunction_zero line 26
  3. theorem OAI.CoarseAssembly.extendedFunction_hasSum line 31
  4. theorem OAI.CoarseAssembly.inclusionVector_apply line 43
  5. theorem OAI.CoarseAssembly.inclusionVector_zero line 47
  6. theorem OAI.CoarseAssembly.inclusionIsometry_single line 50