OAI/Topology/CoarseAssembly/SampledRipsEstimates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounds for the localized finite sums used in homotopy telescoping

  1. theorem OAI.CoarseAssembly.Rips.sampledFiniteSum_partition_sub_norm_le line 18
  2. theorem OAI.CoarseAssembly.Rips.sampledFiniteSum_ample_sub_norm_le line 36