OAI/Topology/CoarseAssembly/SeparatedRips.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Late components are clopen at a fixed Rips scale

This proves the topological component separation required for the changing finite-component winding test in the actual separated coarse union.

  1. theorem OAI.CoarseAssembly.separatedComponent_isometry line 22
  2. theorem OAI.CoarseAssembly.separatedComponent_separation line 30
  3. theorem OAI.CoarseAssembly.separated_closedBall_finite line 44
  4. theorem OAI.CoarseAssembly.lateRipsComponent_openEmbedding line 66

    Source documentation

    The chosen late finite Rips component really is open and closed in the global Rips realization; its inclusion is continuous and proper.

    theorem lateRipsComponent_openEmbedding [∀ j, Fintype (V j)]
    (o : ∀ j, V j) (j : ℕ) (r : ℝ) (hj : r < j) :
    letI := separatedMetric o
…

    Mentions: OAI.CoarseAssembly.separatedMetric