OAI/Topology/CoarseAssembly/ConcreteSpaces.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual base and fibered coarse unions

Both metrics restrict to shortest-path metrics on the components. The fibered union is indexed by base vertices so its Hilbert module has exactly the form used by the finite-fiber transfer theorem.

  1. instance OAI.CoarseAssembly.discGraphMetric line 23
  2. theorem OAI.CoarseAssembly.discGraphMetric_eq line 26
  3. instance OAI.CoarseAssembly.baseUnionMetric line 30
  4. theorem OAI.CoarseAssembly.componentMetric_eq line 32
  5. theorem OAI.CoarseAssembly.baseUnion_uniform_balls line 36
  6. theorem OAI.CoarseAssembly.baseUnion_separated line 46
  7. theorem OAI.CoarseAssembly.componentUnion_uniform_balls line 52
  8. theorem OAI.CoarseAssembly.uniform_balls_of_equiv line 70

    Source documentation

    Transport an exact finite-ball bound across an isometric equivalence.

    theorem uniform_balls_of_equiv {X Y : Type*} [PseudoMetricSpace X] [PseudoMetricSpace Y]
    (e : X ≃ Y) (he : ∀ x y, dist (e x) (e y) = dist x y)
    (hY : UniformFiniteBalls Y) : UniformFiniteBalls X := by
…

    Mentions: OAI.CoarseAssembly.UniformFiniteBalls

  9. theorem OAI.CoarseAssembly.vertexUnion_uniform_balls line 84
  10. theorem OAI.CoarseAssembly.vertexUnion_separated line 92