OAI/Geometry/HyperbolicGroups/Exceptional.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.CoreGeometry.MetricCore.exceptional_radius line 18
  2. def OAI.HyperbolicObstruction.MasterGraph.excC line 35
  3. def OAI.HyperbolicObstruction.MasterGraph.excY line 36
  4. def OAI.HyperbolicObstruction.MasterGraph.excD line 37
  5. def OAI.HyperbolicObstruction.MasterGraph.excI line 38
  6. lemma OAI.HyperbolicObstruction.MasterGraph.exc_not line 40
  7. lemma OAI.HyperbolicObstruction.MasterGraph.exc_admissible line 41
  8. lemma OAI.HyperbolicObstruction.MasterGraph.array_inverse line 60
  9. def OAI.HyperbolicObstruction.MasterGraph.excTest line 69
  10. lemma OAI.HyperbolicObstruction.MasterGraph.excTest_depends line 74
  11. lemma OAI.HyperbolicObstruction.MasterGraph.excTest_bound line 81
  12. theorem OAI.HyperbolicObstruction.MasterGraph.exceptionalTest line 105

    Source documentation

    The source's decisive test is applied to the two actual C fields and loose D field; its test depends only on the indicated two labels.

    theorem exceptionalTest : CoreGeometry.ExceptionalTest (OrbitLimit.catZero O U)
    (fun v => limit (U := U) O A letter hact g hM (.inl v)) := by
…

    Mentions: OAI.HyperbolicObstruction.CoreGeometry.ExceptionalTest, OAI.HyperbolicObstruction.OrbitLimit.catZero, OAI.HyperbolicObstruction.MasterGraph.limit

  13. theorem OAI.HyperbolicObstruction.MasterGraph.impossible_sequence line 145

    Source documentation

    No sequence of consistent literal-master-pattern actions with the sampling conclusions can exist.

    theorem impossible_sequence : False :=
…