OAI/GroupTheory/PolycyclicRecognition/Geometry/GenericWeightDirections.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.genericWeightDirections line 19
2. theorem OAI.PolycyclicRecognition.dense_genericWeightDirections line 24

   Source documentation

   Every nonzero weight cuts out a closed hyperplane with empty interior; the finitely many hyperplanes can be avoided in every open set.

   theorem dense_genericWeightDirections (α : I → W →L[ℝ] ℝ)
       (hα : ∀ i, α i ≠ 0) : Dense (genericWeightDirections α) := by
   …

   Mentions: OAI.PolycyclicRecognition.genericWeightDirections

3. theorem OAI.PolycyclicRecognition.exists_generic_weight_positive line 44

   Source documentation

   A prescribed side of any one weight contains generic directions.

   theorem exists_generic_weight_positive (α : I → W →L[ℝ] ℝ)
       (hα : ∀ i, α i ≠ 0) (i : I) :
       ∃ w ∈ genericWeightDirections α, 0 < α i w := by
   …

   Mentions: OAI.PolycyclicRecognition.genericWeightDirections

4. theorem OAI.PolycyclicRecognition.exists_generic_weight_negative line 60