OAI/Geometry/HyperbolicGroups/FanActivation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.multiplicity_le_card line 18
2. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.maxMultiplicity_le_card line 20
3. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.activation_bound line 27

   Source documentation

   A positive-weight nominal fan is supported either by a selected top slot or by a selected fan triangle. This includes slots omitted by a top boundary.

   lemma activation_bound (h : 0 < D.weight) : 1 ≤ Fintype.card F + D.triangles := by
   …