OAI/Topology/CoarseAssembly/CoefficientDecomposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal decompositions lifted to the spatial vertex modules

  1. theorem OAI.CoarseAssembly.orthogonal_isometries_decompose line 16
  2. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientIsometry_orthogonal line 41
  3. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientIsometry_exhaustive line 51
  4. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_directSum line 74