ConeApexProducer.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.HyperbolicObstruction.ConeSkeleton.SelectedOccurrence line 25
instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 27) line 27
def OAI.HyperbolicObstruction.ConeSkeleton.selectedOccurrence' line 31
def OAI.HyperbolicObstruction.ConeSkeleton.indexedFanData line 39
Source documentation
The actual selected fragment of an actual normalized genus-zero mapped picture supplies EVERY field of the local fan-link data. No apex bound, no triangle-link normality and no contact separation is assumed.
```
def indexedFanData (hs : P.Simple) (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f))
    (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) :
    FanLink.IndexedFanData (ApexInstance n w d c hc f P select b)
      (SelectedTop n w d c hc f P select b) (SelectedOccurrence n w d c hc f P select)
      (fun z => P.Link z.val) where
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.FanLink.IndexedFanData, OAI.HyperbolicObstruction.ConeSkeleton.ApexInstance, OAI.HyperbolicObstruction.ConeSkeleton.SelectedTop, OAI.HyperbolicObstruction.ConeSkeleton.SelectedOccurrence
def OAI.HyperbolicObstruction.ConeSkeleton.actualFanData line 59
theorem OAI.HyperbolicObstruction.ConeSkeleton.actual_apex_bound line 68
Source documentation
The one-fan nominal apex inequality for the actual link extraction and every selection of faces in the picture.
```
theorem actual_apex_bound (hs : P.Simple) (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f))
    (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) :
    let L := actualFanData n w d c hc f P select b hs hm hred hrad
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.actualFanData