OAI/GroupTheory/ArtinCAT0/TriangleMesh.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ArtinCAT0.TriangleMesh line 9

    Source documentation

    Oriented finite triangular incidence data. Faces/edges may have repeated incidences; no topological assumption is built into this record.

    structure TriangleMesh (F V : Type*) where
…
  2. abbrev OAI.ArtinCAT0.TriangleMesh.Dart line 19
  3. def OAI.ArtinCAT0.TriangleMesh.rotate line 21
  4. lemma OAI.ArtinCAT0.TriangleMesh.rotate_apply line 27
  5. lemma OAI.ArtinCAT0.TriangleMesh.rotate_symm_apply line 28
  6. lemma OAI.ArtinCAT0.TriangleMesh.mate_mate line 30
  7. lemma OAI.ArtinCAT0.TriangleMesh.tail_rotate_mate line 32
  8. def OAI.ArtinCAT0.TriangleMesh.turn line 35
  9. lemma OAI.ArtinCAT0.TriangleMesh.turn_apply line 37
  10. lemma OAI.ArtinCAT0.TriangleMesh.tail_turn line 39
  11. def OAI.ArtinCAT0.TriangleMesh.Exact line 45

    Source documentation

    A real edge cocycle is exact. This algebraic formulation allows the fold-deletion proof to avoid any appeal to an unformalized planar theorem.

    def Exact : Prop :=
…
  12. abbrev OAI.ArtinCAT0.TriangleMesh.Edge line 54
  13. def OAI.ArtinCAT0.TriangleMesh.edgeRep line 56
  14. lemma OAI.ArtinCAT0.TriangleMesh.edgeRep_mate line 60
  15. lemma OAI.ArtinCAT0.TriangleMesh.edgeRep_edge line 68
  16. def OAI.ArtinCAT0.TriangleMesh.extend line 72
  17. lemma OAI.ArtinCAT0.TriangleMesh.extend_edge line 75
  18. lemma OAI.ArtinCAT0.TriangleMesh.extend_mate line 78
  19. lemma OAI.ArtinCAT0.TriangleMesh.extend_of_antisymmetric line 86
  20. def OAI.ArtinCAT0.TriangleMesh.edgeDartEquiv line 92
  21. lemma OAI.ArtinCAT0.TriangleMesh.edge_card line 106
  22. def OAI.ArtinCAT0.TriangleMesh.coboundary line 111
  23. lemma OAI.ArtinCAT0.TriangleMesh.extend_coboundary line 116
  24. def OAI.ArtinCAT0.TriangleMesh.boundarySum line 124
  25. lemma OAI.ArtinCAT0.TriangleMesh.boundarySum_coboundary line 141
  26. lemma OAI.ArtinCAT0.TriangleMesh.exact_iff line 150
  27. lemma OAI.ArtinCAT0.TriangleMesh.sum_boundarySum line 172
  28. lemma OAI.ArtinCAT0.TriangleMesh.exact_euler_inequality line 180
  29. lemma OAI.ArtinCAT0.TriangleMesh.tail_iterate_turn line 203
  30. lemma OAI.ArtinCAT0.TriangleMesh.six_turns_injective line 209
  31. lemma OAI.ArtinCAT0.TriangleMesh.degree_at_least_six line 235
  32. theorem OAI.ArtinCAT0.TriangleMesh.exists_link_backtrack line 260

    Source documentation

    Curvature forces a backtrack in any nonempty exact triangular mesh. Only finite linear algebra, incidence counting, and the checked finite link are used here, in place of a black-box planar Euler theorem.

    theorem exists_link_backtrack [Fintype F] [Fintype V] [Nonempty F]
    (he : M.Exact) (hs : Function.Surjective M.tail)
    (direction : Dart (F := F) → LinkDirection)
…

    Mentions: OAI.ArtinCAT0.TriangleMesh.Dart, OAI.ArtinCAT0.LinkDirection