OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanAllowedProfileCompactness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact containment for all allowed sheet suffixes

  1. theorem OAI.PolycyclicRecognition.exists_compact_allowed_cartan_profiles line 28

    Source documentation

    After deleting finitely many scales, one compact profile family contains every sample and every allowed suffix in the enlarged word box. The only suffix assumption is its vanishing coordinate-error envelope.

    theorem exists_compact_allowed_cartan_profiles
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput