OAI/Topology/CoarseAssembly/FiberEmbedding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The constant-fiber spatial isometry

This is the actual map from the base Roe module to the fibered Roe module. On singleton boundary fibers it is exactly the coordinate inclusion.

  1. def OAI.CoarseAssembly.fiberEmbedding line 20
  2. theorem OAI.CoarseAssembly.fiberEmbedding_apply line 24
  3. theorem OAI.CoarseAssembly.fiberEmbedding_singleton line 28
  4. def OAI.CoarseAssembly.fiberProjection line 43
  5. theorem OAI.CoarseAssembly.fiberProjection_idempotent line 46
  6. theorem OAI.CoarseAssembly.fiberProjection_selfAdjoint line 51
  7. theorem OAI.CoarseAssembly.fiberProjection_norm_le line 55