OAI/GroupTheory/PolycyclicRecognition/Algebra/TwoImageLimits.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous limits of two box embeddings

The bounded embeddings and their bounded generator preimages are retained alongside the normalized Lie law. Thus every limiting generator belongs to one of the limiting images, and the full alternating product is submersive.

  1. abbrev OAI.PolycyclicRecognition.TwoImageData line 20
  2. def OAI.PolycyclicRecognition.TwoImageData.generatorsCovered line 25
  3. def OAI.PolycyclicRecognition.HasSubmersiveTwoImageSubsequence line 28
  4. theorem OAI.PolycyclicRecognition.isClosed_twoImageData_generatorsCovered line 40
  5. theorem OAI.PolycyclicRecognition.exists_submersive_twoImage_limit line 52