OAI/Topology/CoarseAssembly/RipsInclusionNaturality.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite-Rips localization respects an actual vertex inclusion

  1. def OAI.CoarseAssembly.Rips.inclusionFunctionHom line 19
  2. theorem OAI.CoarseAssembly.Rips.inclusionFunctionHom_sqrt line 23
  3. theorem OAI.CoarseAssembly.Rips.inclusionFunctionHom_sqrt_zero line 31
  4. def OAI.CoarseAssembly.Rips.includedCycle line 39
  5. theorem OAI.CoarseAssembly.Rips.includedCycle_unital line 43
  6. theorem OAI.CoarseAssembly.Rips.includedCycle_representedSqrt line 49
  7. theorem OAI.CoarseAssembly.Rips.includedCycle_representedSqrt_zero line 56
  8. theorem OAI.CoarseAssembly.Rips.ripsSpatialOperator_inclusion line 62