OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanUniformBoxProfiles.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Profiles fixed before the small enlargement is chosen

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_compact_measurable_box_profiles line 31

    Source documentation

    Choose a compact family and one Borel profile map for every allowed suffix in a fixed larger box. No particular chain or smaller enlargement is chosen until after this family has been fixed.

    theorem exists_compact_measurable_box_profiles
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput