OAI/Topology/CoarseAssembly/CoefficientInclusion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Ample coefficient transport commutes with vertex inclusion

  1. theorem OAI.CoarseAssembly.DiscreteRoe.coefficientIsometry_inclusion line 18
  2. theorem OAI.CoarseAssembly.Rips.ampleRipsOperator_inclusion line 40