OAI/Topology/CoarseAssembly/LateRipsCoarsening.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coarsening commutes with restriction to every sufficiently late component

  1. theorem OAI.CoarseAssembly.Rips.separatedRips_coarsen_preimage line 20
  2. theorem OAI.CoarseAssembly.Rips.lateRipsFunctionHom_coarsen line 36