OAI/Geometry/HyperbolicGroups/ActualWeights.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.top_count_le_slot line 26
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.indexed_weight_congr line 49
3. def OAI.HyperbolicObstruction.ConeSkeleton.actualWeights line 57

   Source documentation

   Weights are the literal selected-face multiplicities and maximum of actual apex count / same-top slot multiplicity. No contact capacity is a field.

   def actualWeights : (occurrenceShape n w).Weights (v := Fintype.card (Six n d)) where
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.occurrenceShape, OAI.HyperbolicObstruction.ConeSkeleton.Six

4. lemma OAI.HyperbolicObstruction.ConeSkeleton.actual_position_capacity line 69