OAI/Topology/CoarseAssembly/BoundedFamilySubdivision.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Component-dependent subdivisions with uniformly close sampled Roe operators

  1. def OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.samplingTolerance line 20
  2. theorem OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.samplingTolerance_pos line 24
  3. theorem OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.samplingTolerance_estimate line 31
  4. theorem OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.exists_small_subdivision line 40
  5. structure OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.SmallSubdivision line 65
  6. def OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.smallSubdivision line 76
  7. theorem OAI.CoarseAssembly.Rips.BoundedFamilyHomotopy.sampled_boundary_eq line 83