OAI/Topology/CoarseAssembly/ConcreteIndexFamilies.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The three constructed analytic index families used by the counterexample

  1. theorem OAI.CoarseAssembly.boundaryReindex_isometry line 29
  2. def OAI.CoarseAssembly.boundaryInverseCoarsening line 35
  3. def OAI.CoarseAssembly.constructedBoundaryIndex line 41
  4. def OAI.CoarseAssembly.separatedBaseEq line 44
  5. def OAI.CoarseAssembly.baseReindexRoeHom line 47
  6. def OAI.CoarseAssembly.constructedBaseIndex line 52