OAI/Topology/CoarseAssembly/RipsUnitaryLocalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unitary equivalence commutes with finite-Rips localization

  1. theorem OAI.CoarseAssembly.isometricExtension_equiv line 16
  2. theorem OAI.CoarseAssembly.DiscreteRoe.partitionIsometry_apply line 34
  3. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientIsometry_comp line 40
  4. theorem OAI.CoarseAssembly.Rips.ripsCompression_unitary line 57
  5. theorem OAI.CoarseAssembly.Rips.partitionIsometry_unitary line 70
  6. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_unitary line 87