OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTiledSourceBridge.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The metric contact bridge on the actual source probability cell

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.TiledProbeChainData.exists_source_cell_bridge line 64

    Source documentation

    The published exponential representation yields the bridge for the actual quotient section retained by the tiled source cell. The original center and the independently selected sample are both preserved.

    theorem TiledProbeChainData.exists_source_cell_bridge
    [SimplyConnectedSpace G] [IsIsometricSMul G G]
    (hExpG : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput