OAI/GroupTheory/Hyperbolic/Words.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.Release075.WordPath line 9
  2. def OAI.Release075.reverseWord line 14
  3. theorem OAI.Release075.reverseWord_nil line 16
  4. theorem OAI.Release075.reverseWord_cons line 17
  5. theorem OAI.Release075.reverseWord_append line 20
  6. theorem OAI.Release075.reverseWord_reverse line 24
  7. theorem OAI.Release075.WordPath.source line 33
  8. theorem OAI.Release075.WordPath.append line 36
  9. theorem OAI.Release075.WordPath.singleton line 42
  10. theorem OAI.Release075.WordPath.reverse line 45
  11. theorem OAI.Release075.Fillable.erase_reverse line 63

    Source documentation

    Erase a reversed path followed by the path, in any boundary context.

    theorem erase_reverse (u v p : List E)
    (h : Fillable flip color face (u ++ reverseWord flip p ++ p ++ v)) :
    Fillable flip color face (u++v) := by
…

    Mentions: OAI.Release075.Fillable, OAI.Release075.reverseWord

  12. theorem OAI.Release075.Fillable.stemPath line 79

    Source documentation

    Attach a whole typed stem; each corner identification is type checked.

    theorem stemPath {a b : V} {p w : List E} (hp : WordPath flip color a b p)
    (hw : WordPath flip color b b w) (h : Fillable flip color face w) :
    Fillable flip color face (p++w++reverseWord flip p) := by
…

    Mentions: OAI.Release075.WordPath, OAI.Release075.Fillable, OAI.Release075.reverseWord

  13. theorem OAI.Release075.Fillable.palindrome line 93
  14. def OAI.Release075.FilledBetween line 101

    Source documentation

    Filling the two paths glued along their common endpoints.

    def FilledBetween (flip : E → E) (color : E → V) (face : E → E → E → Prop)
    (p q : List E) : Prop := Fillable flip color face (p++reverseWord flip q)
…

    Mentions: OAI.Release075.Fillable, OAI.Release075.reverseWord

  15. theorem OAI.Release075.FilledBetween.refl line 111
  16. theorem OAI.Release075.FilledBetween.symm line 115
  17. theorem OAI.Release075.FilledBetween.trans line 121
  18. theorem OAI.Release075.FilledBetween.whiskerLeft line 136
  19. theorem OAI.Release075.FilledBetween.whiskerRight line 144
  20. abbrev OAI.Release075.BlockPresentation.OrientedEdge line 161
  21. def OAI.Release075.BlockPresentation.flipEdge line 163
  22. theorem OAI.Release075.BlockPresentation.flipEdge_flipEdge line 165
  23. def OAI.Release075.BlockPresentation.edgeTarget line 169
  24. theorem OAI.Release075.BlockPresentation.edgeTarget_ne line 177
  25. def OAI.Release075.BlockPresentation.arrowLabel line 181
  26. def OAI.Release075.BlockPresentation.orientedLabel line 186
  27. theorem OAI.Release075.BlockPresentation.orientedLabel_reverse line 191
  28. theorem OAI.Release075.BlockPresentation.orientedLabel_target line 196
  29. theorem OAI.Release075.BlockPresentation.orientedLabel_source line 205
  30. def OAI.Release075.BlockPresentation.rawWord line 210
  31. theorem OAI.Release075.BlockPresentation.rawWord_nil line 217
  32. theorem OAI.Release075.BlockPresentation.rawWord_comp line 219
  33. theorem OAI.Release075.BlockPresentation.rawWord_path_comp line 231
  34. theorem OAI.Release075.BlockPresentation.rawWord_toPath line 241
  35. theorem OAI.Release075.BlockPresentation.rawWord_reverse line 244
  36. theorem OAI.Release075.BlockPresentation.rawWord_typed line 256
  37. def OAI.Release075.BlockPresentation.orientedL line 268
  38. def OAI.Release075.BlockPresentation.orientedX line 270
  39. def OAI.Release075.BlockPresentation.orientedR line 271
  40. inductive OAI.Release075.BlockPresentation.TriangleFace line 274
  41. theorem OAI.Release075.BlockPresentation.TriangleFace.rotate line 288
  42. theorem OAI.Release075.BlockPresentation.TriangleFace.mirror line 298
  43. theorem OAI.Release075.BlockPresentation.rawMove_filled line 308
  44. theorem OAI.Release075.BlockPresentation.rawHomotopic_filled line 326
  45. theorem OAI.Release075.BlockPresentation.nullhomotopic_fillable line 346
  46. theorem OAI.Release075.BlockPresentation.rectangle_fillable_of_eq_one line 353

    Source documentation

    The actual presented rectangular word, if trivial, has a finite labelled planar triangular filling. This lemma has no geometric hypothesis.

    theorem rectangle_fillable_of_eq_one (i : I) (u u' v v' : Fin r)
    (h : d.x i u v * (d.x i u' v)⁻¹ * d.x i u' v' * (d.x i u v')⁻¹ = 1) :
    Fillable d.flipEdge d.edgeTarget d.TriangleFace
      [d.orientedX i u v, d.flipEdge (d.orientedX i u' v),
       d.orientedX i u' v', d.flipEdge (d.orientedX i u v')] := by
…

    Mentions: OAI.Release075.Fillable

  47. def OAI.Release075.BlockPresentation.vertexColor line 365
  48. theorem OAI.Release075.BlockPresentation.TriangleFace.colors line 371
  49. theorem OAI.Release075.BlockPresentation.TriangleFace.typed line 376
  50. theorem OAI.Release075.BlockPresentation.TriangleFace.unique_aux line 382
  51. theorem OAI.Release075.BlockPresentation.TriangleFace.unique line 421