OAI/Topology/CoarseAssembly/ControlledRipsCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The analytic coordinates of a controlled family class

  1. def OAI.CoarseAssembly.Rips.controlledCoordinateFree line 16
  2. theorem OAI.CoarseAssembly.Rips.controlledCoordinateFree_relation line 20
  3. def OAI.CoarseAssembly.Rips.controlledCoordinate line 39

    Source documentation

    Ordinary analytic K-homology of each compact component. Injectivity or surjectivity of the resulting coordinate family is not asserted here.

    def controlledCoordinate (i : ℕ) : ControlledK Q r →+ OddK C(Point (Q i) r, ℂ) :=
…

    Mentions: OAI.CoarseAssembly.Rips.ControlledK, OAI.CoarseAssembly.Rips.Point

  4. theorem OAI.CoarseAssembly.Rips.controlledCoordinate_class line 43