OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryShadow.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constructed boundary maps with a common compact shadow

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_boundary_map_with_compact_shadow line 38

    Source documentation

    Uniform sublinear height control constructs the boundary map and its common compact shadow. Representative independence, convergence and continuity of each ambient action are supplied by the preceding proofs.

    theorem exists_boundary_map_with_compact_shadow
    [SimplyConnectedSpace G]
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput