OAI/GroupTheory/PolycyclicRecognition/Algebra/CenteredSourceTerminals.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.relativeTupleTerminals line 17
2. theorem OAI.PolycyclicRecognition.isCompact_relativeTupleTerminals line 22
3. theorem OAI.PolycyclicRecognition.centered_image_terminal_mem line 31

   Source documentation

   A source terminal relative to the original starting point maps to the terminal coordinate of the centered tuple under the normalized pair.

   theorem centered_image_terminal_mem {h : ℕ} {Λ : ℝ≥0}
       (p : NormalizedPair G Λ) (ι : N → G) (origin base pivot : G)
       (last : Fin h) (S : Set (Fin h → N)) {y : Fin h → G}
       (hy : y ∈ (fun v : Fin h → N => fun i =>
         basedImage p.val.1 origin (base * ι (v i) * pivot)) '' S) :
       ∃ z ∈ relativeTupleTerminals ι origin base pivot last S,
         y last = (normalizedTranslate origin p).val.1 z := by
   …

   Mentions: OAI.PolycyclicRecognition.NormalizedPair, OAI.PolycyclicRecognition.basedImage, OAI.PolycyclicRecognition.relativeTupleTerminals, OAI.PolycyclicRecognition.normalizedTranslate