OAI/GroupTheory/PolycyclicRecognition/Algebra/TemplateThickeningLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing the final height-template enlargement

  1. theorem OAI.PolycyclicRecognition.SupportDatum.le_templateSupport_of_thickenings line 18

    Source documentation

    An exponent bounded by every positive thickening is bounded by the original compact template.

    theorem le_templateSupport_of_thickenings {E : Set W} (hE : IsCompact E)
    (hne : E.Nonempty) {p : ℝ}
    (h : ∀ ε : ℝ, 0 < ε → p ≤ D.templateSupport (E + closedBall 0 ε)) :
    p ≤ D.templateSupport E := by
…