OAI/Geometry/HyperbolicGroups/RelativeWeights.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.top_count_le_slot line 27
2. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.indexed_weight_congr line 50
3. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualWeights line 58

   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.RelDisk.actual_position_capacity line 70