OAI/Combinatorics/CompleteCrossing/Plane.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Planar segment geometry, affine parametrizations, and oriented arc directions.

  1. theorem OAI.Paper170.segmentPoint_eq line 22
  2. theorem OAI.Paper170.det2_eq line 25
  3. theorem OAI.Paper170.segmentIntersection_eq_segmentCrossingSign line 27
  4. theorem OAI.Paper170.segmentIntersection_swap line 40
  5. theorem OAI.Paper170.TransversePolygons.segmentPairTransverse line 45
  6. theorem OAI.Paper170.closed_polygon_intersection_zero line 78
  7. def OAI.Paper170.ofZarankiewiczParametrization line 86

    Source documentation

    Transfer a genuine affine parametrization, retaining the identical path and knots.

    def ofZarankiewiczParametrization {a b : Plane} {γ : Path a b}
    (P : Zarankiewicz.PolygonalParametrization γ) : PolygonalParametrization γ where
…

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

  8. theorem OAI.Paper170.simple_polygonal_replacement line 118
  9. theorem OAI.Paper170.squaredLength_pos line 127
  10. theorem OAI.Paper170.inversion_involutive line 136
  11. theorem OAI.Paper170.inversion_fixes_circle line 150
  12. def OAI.Paper170.toZarankiewiczParametrization line 166
  13. theorem OAI.Paper170.vertices_toZarankiewicz line 190
  14. theorem OAI.Paper170.PolygonalParametrization.segment_mem_interior line 194
  15. theorem OAI.Paper170.PolygonalParametrization.vertices_first line 207
  16. theorem OAI.Paper170.PolygonalParametrization.vertices_last line 211
  17. theorem OAI.Paper170.PolygonalParametrization.direction_ne_zero line 215
  18. theorem OAI.Paper170Geometry.sum_eq_sum_of_unique_match line 232
  19. theorem OAI.Paper170Geometry.segmentCrossingSign_ne_zero_iff line 267
  20. theorem OAI.Paper170Geometry.meeting_of_mem_openSegments line 272
  21. theorem OAI.Paper170Geometry.openSegments_inter_subsingleton line 279
  22. theorem OAI.Paper170Geometry.segmentCrossingSign_eq_of_pos_directions line 286
  23. theorem OAI.Paper170Geometry.polygonIntersection_eq_fin_sum line 299
  24. theorem OAI.Paper170.path_reparametrization line 320

    Source documentation

    Two injective paths with the same endpoints and trace have the same orientation.

    theorem path_reparametrization {a b : Plane} (γ η : Path a b)
    (hγ : Function.Injective γ) (hη : Function.Injective η)
    (hrange : Set.range γ = Set.range η) :
    ∃ f : unitInterval → unitInterval, Continuous f ∧ StrictMono f ∧
      f 0 = 0 ∧ f 1 = 1 ∧ ∀ t, γ (f t) = η t := by
…

    Mentions: OAI.Paper170.Plane

  25. lemma OAI.Paper170.intervalSegment_lt_iff line 357
  26. lemma OAI.Paper170.segmentPoint_sub_segmentPoint line 367
  27. theorem OAI.Paper170.path_segments_direction line 373

    Source documentation

    Oriented affine pieces of two parametrizations of the same simple arc have positively proportional directions whenever they overlap to the right.

    theorem path_segments_direction {a b : Plane} (γ η : Path a b)
    (hγ : Function.Injective γ) (hη : Function.Injective η)
    (hrange : Set.range γ = Set.range η)
    (a₀ a₁ b₀ b₁ : unitInterval) (ha : a₀ < a₁) (hb : b₀ < b₁)
    (A B C D : Plane)
    (hγseg : ∀t, γ (intervalSegment a₀ a₁ t) = Paper170.segmentPoint A B t.val)
    (hηseg : ∀t, η (intervalSegment b₀ b₁ t) = Paper170.segmentPoint C D t.val)
    (p q : unitInterval) (hp : p < 1) (hq : q < 1)
    (hpoint : Paper170.segmentPoint A B p.val = Paper170.segmentPoint C D q.val) :
    ∃ r : ℝ, 0 < r ∧ D-C = r • (B-A) := by
…

    Mentions: OAI.Paper170.Plane, OAI.Paper170.segmentPoint

  28. theorem OAI.Paper170.path_segments_direction_of_mem line 418

    Source documentation

    Interior overlap is sufficient for the positive direction comparison.

    theorem path_segments_direction_of_mem {a b : Plane} (γ η : Path a b)
    (hγ : Function.Injective γ) (hη : Function.Injective η)
    (hrange : Set.range γ = Set.range η)
    (a₀ a₁ b₀ b₁ : unitInterval) (ha : a₀ < a₁) (hb : b₀ < b₁)
    (A B C D : Plane)
    (hγseg : ∀t, γ (intervalSegment a₀ a₁ t) = Paper170.segmentPoint A B t.val)
    (hηseg : ∀t, η (intervalSegment b₀ b₁ t) = Paper170.segmentPoint C D t.val)
    (x : Plane) (hx : x ∈ openSegmentTrace A B) (hy : x ∈ openSegmentTrace C D) :
    ∃ r : ℝ, 0 < r ∧ D-C = r • (B-A) := by
…

    Mentions: OAI.Paper170.Plane, OAI.Paper170.segmentPoint

  29. lemma OAI.Paper170.reverse_affine_piece line 444
  30. theorem OAI.Paper170.path_final_segments_direction line 459