OAI/Topology/CoarseAssembly/ConcreteTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The transfer on the actual coarse spaces

All metric and inter-fiber hypotheses have been discharged. Only the averaging projection approximation remains in this intermediate theorem; it is an own-paper obligation, not an assumed published theorem.

  1. theorem OAI.CoarseAssembly.UniformFiniteBalls.finite_closedBall line 19
  2. theorem OAI.CoarseAssembly.concrete_transfer_of_approximation line 31