OAI/Topology/CoarseAssembly/PartitionIsometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The Hilbert-space isometry of a finite square partition

  1. theorem OAI.CoarseAssembly.DiscreteRoe.coordinate_partitionMap line 16
  2. theorem OAI.CoarseAssembly.DiscreteRoe.partitionMap_adjoint line 22
  3. theorem OAI.CoarseAssembly.DiscreteRoe.partitionMap_adjoint_comp line 26
  4. theorem OAI.CoarseAssembly.DiscreteRoe.partitionIsometry_toContinuousLinearMap line 33