OAI/Geometry/ConjugatePoints/ThreeManifold.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The universal-cover shear obstruction and the three-manifold existence theorem.

  1. lemma OAI.ThreeManifold.CompactMetric.lowPoint_clip line 19
  2. lemma OAI.ThreeManifold.CompactMetric.blockMap_low line 22
  3. lemma OAI.ThreeManifold.CompactMetric.compact_fiber_periodic line 28
  4. lemma OAI.ThreeManifold.CompactMetric.block_fiber_low_nontrivial line 36
  5. theorem OAI.ThreeManifold.CompactMetric.fiberClass_ne_one line 62
  6. theorem OAI.ThreeManifold.RiemannianCoordinates.universalMetric_exists_CN line 81
  7. def OAI.ThreeManifold.RiemannianCoordinates.universalCN line 102
  8. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_radial_dist_of_le line 118
  9. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_radial_dist line 139
  10. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_radial_isometry line 149
  11. lemma OAI.ThreeManifold.RiemannianCoordinates.universalMetric_segments line 166
  12. def OAI.ThreeManifold.RiemannianCoordinates.npcDeckIsometry line 187
  13. theorem OAI.ThreeManifold.RiemannianCoordinates.npc_deck_shear_impossible line 196
  14. def OAI.ThreeManifold.LoopTopology.groupBasepointEq line 226
  15. theorem OAI.ThreeManifold.CompactMetric.realCompact_noNPC line 233
  16. theorem OAI.ThreeManifold.main_theorem line 260

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: OAI.ThreeManifold.MainStatement

    Proof uses: Real, And, LT.lt, OfNat.ofNat, LE.le, HDiv.hDiv, Nat, Membership.mem, Set, Set.Ioc, OAI.ThreeManifold.NoConjugatePoints, OAI.ThreeManifold.GluedConstruction.Manifold, OAI.ThreeManifold.CompactMetric.realCompactMetric, Exists, OAI.ThreeManifold.CompactMetric.exists_uniform_compact_noConjugatePoints, And.intro, Exists.intro, TopologicalSpace, T2Space, SecondCountableTopology and 18 more

    51 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: ComparatorChallenges/ConjugatePoints.lean:109 (same statement text; different proof or body). Qualify references as OAI.ThreeManifold.main_theorem@path.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.