OAI/GroupTheory/PolycyclicRecognition/Analysis/BadCharacterCompactness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compactness of the bad unit-character set

The full positive-identity criterion makes the good region open. Its complement on the unit sphere is the compact set used in the convex tameness argument.

  1. def OAI.PolycyclicRecognition.positiveIdentityRegion line 19
  2. def OAI.PolycyclicRecognition.badUnitCharacters line 22
  3. theorem OAI.PolycyclicRecognition.positiveIdentityRegion_open line 27
  4. theorem OAI.PolycyclicRecognition.badUnitCharacters_eq_sdiff line 36
  5. theorem OAI.PolycyclicRecognition.badUnitCharacters_compact line 57