OAI/Topology/CoarseAssembly/DirectSumIntertwining.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Direct-sum inclusions intertwine the actual localized operators

  1. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_apply_left line 14
  2. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_apply_right line 23
  3. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_directSum_left line 41
  4. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_directSum_right line 57