OAI/Topology/EilenbergGanea/Seed.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EilenbergGanea.seedWord line 14

    Source documentation

    false names x; true names y. The second Boolean is the positive sign.

    Also declared: ComparatorChallenges/EilenbergGanea.lean:12 (same declaration text).

    def seedWord : Bool → List (Bool × Bool)
  | false => [(false, true), (false, true), (true, false), (true, false),
      (true, false), (true, false), (true, false)]
  | true => [(false, true), (false, true), (true, true), (false, false),
      (true, true), (false, false), (true, true), (false, false)]

/-- Numbers of sectors in the two coned boundary polygons. -/
  2. def OAI.EilenbergGanea.boundaryLength line 21

    Source documentation

    Numbers of sectors in the two coned boundary polygons.

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:18 (different declaration text). Qualify references as OAI.EilenbergGanea.boundaryLength@path.

    def boundaryLength (r : Bool) : ℕ := 3 * (seedWord r).length

    Mentions: OAI.EilenbergGanea.seedWord

  3. abbrev OAI.EilenbergGanea.RoseVertex line 23

    Also declared: ComparatorChallenges/EilenbergGanea.lean:20 (same declaration text).

  4. abbrev OAI.EilenbergGanea.SeedVertex line 24

    Also declared: ComparatorChallenges/EilenbergGanea.lean:21 (same declaration text).

  5. abbrev OAI.EilenbergGanea.CircleEdge line 25

    Also declared: ComparatorChallenges/EilenbergGanea.lean:22 (same declaration text).

  6. abbrev OAI.EilenbergGanea.Sector line 26

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:23 (same statement text; different proof or body). Qualify references as OAI.EilenbergGanea.Sector@path.

  7. abbrev OAI.EilenbergGanea.SeedEdge line 27

    Also declared: ComparatorChallenges/EilenbergGanea.lean:24 (same declaration text).

  8. abbrev OAI.EilenbergGanea.SeedCell line 28

    Also declared: ComparatorChallenges/EilenbergGanea.lean:25 (same declaration text).

  9. def OAI.EilenbergGanea.circleStart line 30

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:27 (different declaration text). Qualify references as OAI.EilenbergGanea.circleStart@path.

  10. def OAI.EilenbergGanea.circleEnd line 33

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:30 (different declaration text). Qualify references as OAI.EilenbergGanea.circleEnd@path.

  11. def OAI.EilenbergGanea.sectorLetter line 36

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:33 (different declaration text). Qualify references as OAI.EilenbergGanea.sectorLetter@path.

  12. def OAI.EilenbergGanea.sectorCircleEdge line 42

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:39 (different declaration text). Qualify references as OAI.EilenbergGanea.sectorCircleEdge@path.

  13. def OAI.EilenbergGanea.sectorStart line 47

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:44 (different declaration text). Qualify references as OAI.EilenbergGanea.sectorStart@path.

  14. def OAI.EilenbergGanea.nextSector line 51

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:48 (different declaration text). Qualify references as OAI.EilenbergGanea.nextSector@path.

  15. def OAI.EilenbergGanea.edgeVertices line 55

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:52 (different declaration text). Qualify references as OAI.EilenbergGanea.edgeVertices@path.

  16. def OAI.EilenbergGanea.sectorEdges line 59

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:56 (different declaration text). Qualify references as OAI.EilenbergGanea.sectorEdges@path.

  17. def OAI.EilenbergGanea.sectorVertices line 62

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:59 (different declaration text). Qualify references as OAI.EilenbergGanea.sectorVertices@path.

  18. def OAI.EilenbergGanea.properFace line 66

    Source documentation

    Proper cell-face incidence, including vertices of closed triangles.

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:62 (different declaration text). Qualify references as OAI.EilenbergGanea.properFace@path.

    def properFace : SeedCell → SeedCell → Prop
  | .inl v, .inr (.inl e) => v ∈ edgeVertices e
  | .inl v, .inr (.inr s) => v ∈ sectorVertices s
  | .inr (.inl e), .inr (.inr s) => e ∈ sectorEdges s
  | _, _ => False

    Mentions: OAI.EilenbergGanea.SeedCell

  19. def OAI.EilenbergGanea.seedGraph line 72

    Distinct definitions of this name: ComparatorChallenges/EilenbergGanea.lean:69 (same statement text; different proof or body). Qualify references as OAI.EilenbergGanea.seedGraph@path.

  20. def OAI.EilenbergGanea.seedBase line 87

    Source documentation

    The vertex of the rose common to its two circles.

    def seedBase : SeedCell := .inl (.inl none)

    Mentions: OAI.EilenbergGanea.SeedCell

  21. theorem OAI.EilenbergGanea.seed_vertex_edge_adj line 89
  22. theorem OAI.EilenbergGanea.seed_edge_sector_adj line 92
  23. theorem OAI.EilenbergGanea.rose_vertex_reachable line 95
  24. def OAI.EilenbergGanea.firstSector line 117
  25. theorem OAI.EilenbergGanea.seed_vertex_reachable line 120
  26. theorem OAI.EilenbergGanea.seed_edge_reachable line 133
  27. theorem OAI.EilenbergGanea.seed_cell_reachable line 145
  28. theorem OAI.EilenbergGanea.seed_connected line 155