OAI/Geometry/HyperbolicGroups/RelativeApexProducer.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedOccurrence line 23
  2. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 25) line 25
  3. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedOccurrence' line 29
  4. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.indexedFanData line 37

    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 (frozen n w d ell hell word c hc f))
    (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) :
    FanLink.IndexedFanData (ApexInstance n w d ell hell word c hc f P select b)
      (SelectedTop n w d ell hell word c hc f P select b) (SelectedOccurrence n w d ell hell word c hc f P select)
      (fun z => P.Link z.val) where
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.FanLink.IndexedFanData, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.ApexInstance, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedTop, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.SelectedOccurrence

  5. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualFanData line 57
  6. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_apex_bound line 66

    Source documentation

    Source03's complete one-fan nominal apex inequality, now for the actual link extraction, and for EVERY selection of source faces in the picture.

    theorem actual_apex_bound (hs : P.Simple) (hm : P.FrozenMapped (frozen n w d ell hell word c hc f))
    (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) :
    let L := actualFanData n w d ell hell word c hc f P select b hs hm hred hrad
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualFanData