LocalGeometry.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Local straightness and transversality of normalized drawings.

structure OAI.Paper170Geometry.NoAdjacentCrossings line 20
structure OAI.Paper170Geometry.LocallyStraightAt line 27
structure OAI.Paper170Geometry.LocallyStraightCrossings line 32
structure OAI.Paper170Geometry.LocallyTransverseCrossings line 38
theorem OAI.Paper170Geometry.normalized_noAdjacent line 48

theorem OAI.Paper170Geometry.parametrization_knot_interval line 64

Source documentation

A point away from the subdivision knots lies strictly inside one piece.

theorem parametrization_knot_interval {a b : Paper170.Plane} {γ : Path a b}
    (P : Paper170.PolygonalParametrization γ) (t : unitInterval)
    (ht : t ∈ Ioo (0 : unitInterval) 1) (hne : ∀i, t ≠ P.knot i) :
    ∃i : Fin P.pieces, P.knot i.castSucc < t ∧ t < P.knot i.succ := by
…

Mentions: OAI.Paper170.Plane, OAI.Paper170.PolygonalParametrization

theorem OAI.Paper170Geometry.parametrization_open_piece line 82

Source documentation

The open part of a subdivided path is exactly its open segment.

theorem parametrization_open_piece {a b : Paper170.Plane} {γ : Path a b}
    (P : Paper170.PolygonalParametrization γ) (i : Fin P.pieces) :
    γ '' Ioo (P.knot i.castSucc) (P.knot i.succ) =
      openSegmentTrace (P.vertices i.val) (P.vertices (i.val+1)) := by
…

Mentions: OAI.Paper170.Plane, OAI.Paper170.PolygonalParametrization

theorem OAI.Paper170Geometry.locallyStraightAt_of_not_knot line 111

Source documentation

An injective polygonal path is locally a straight segment away from its knots.

theorem locallyStraightAt_of_not_knot {Vertex Edge : Type} {graph : Paper170.Graph Vertex Edge}
    (D : Paper170.ContinuousDrawing graph) (e : Edge)
    (P : Paper170.PolygonalParametrization (D.edge e)) (t : unitInterval)
    (ht : t ∈ Ioo (0 : unitInterval) 1) (hne : ∀i, t ≠ P.knot i) :
    LocallyStraightAt D e (D.edge e t) := by
…

Mentions: OAI.Paper170.PolygonalParametrization, OAI.Paper170Geometry.LocallyStraightAt

theorem OAI.Paper170Geometry.normalized_locallyStraight line 142

theorem OAI.Paper170Geometry.properCrossing_locally_unique line 168

Source documentation

A crossing chart makes the local intersection a single point.

theorem properCrossing_locally_unique (A B : Set Paper170.Plane) (x : Paper170.Plane)
    (h : Paper170.ProperCrossing A B x) :
    ∃U : Set Paper170.Plane, IsOpen U ∧ x ∈ U ∧
      ∀y ∈ U, y ∈ A → y ∈ B → y = x := by
…

Mentions: OAI.Paper170.Plane

theorem OAI.Paper170Geometry.local_segment_directions_ne_zero line 182

Source documentation

Two straight segments meeting locally only once have independent directions.

theorem local_segment_directions_ne_zero (a b c d x : Plane)
    (hab : a ≠ b) (hcd : c ≠ d)
    (hxab : x ∈ openSegmentTrace a b) (hxcd : x ∈ openSegmentTrace c d)
    (U : Set Plane) (hU : IsOpen U) (hxU : x ∈ U)
    (hunique : ∀y ∈ U, y ∈ openSegmentTrace a b → y ∈ openSegmentTrace c d → y=x) :
    det2 (b-a) (d-c) ≠ 0 := by
…

theorem OAI.Paper170Geometry.locallyTransverse_of_locallyStraight line 228
Source documentation
Local straightness and the actual crossing charts imply transversality.
```
theorem locallyTransverse_of_locallyStraight {Vertex Edge : Type} {graph : Paper170.Graph Vertex Edge}
    (D : Paper170.AdmissibleDrawing graph) (h : LocallyStraightCrossings D) :
    LocallyTransverseCrossings D := by
…
```
Mentions: OAI.Paper170Geometry.LocallyStraightCrossings, OAI.Paper170Geometry.LocallyTransverseCrossings
theorem OAI.Paper170Geometry.normalized_locallyTransverse line 245