Point visibility in the real plane
Lax570090.Geometry · concepts/Lax570090/Geometry.lean · lax-570090
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
A pair of distinct points of a finite planar point set is visible when the open segment joining it contains no point of the ambient set. This module also defines the visibility graph and the two geometric alternatives used in the headline theorem.
Concept map
Lean source view on GitHub
| 1 | import Mathlib.Analysis.Convex.Segment |
| 2 | import Mathlib.Combinatorics.SimpleGraph.Basic |
| 3 | import Mathlib.Data.Real.Basic |
| 4 | import Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Point visibility in the real plane |
| 9 | type: definition |
| 10 | --- |
| 11 | A pair of distinct points of a finite planar point set is visible when the |
| 12 | open segment joining it contains no point of the ambient set. This module |
| 13 | also defines the visibility graph and the two geometric alternatives used in |
| 14 | the headline theorem. |
| 15 | -/ |
| 16 | |
| 17 | namespace Lax570090.Geometry |
| 18 | |
| 19 | /-- The real affine plane, represented by Cartesian coordinates. -/ |
| 20 | abbrev Point := ℝ × ℝ |
| 21 | |
| 22 | /-- The signed twice-area of the oriented triangle `p q r`. -/ |
| 23 | def turn (p q r : Point) : ℝ := |
| 24 | (q.1 - p.1) * (r.2 - p.2) - (q.2 - p.2) * (r.1 - p.1) |
| 25 | |
| 26 | /-- `p` and `q` see one another with respect to the ambient finite set `P`. -/ |
| 27 | def Visible (P : Finset Point) (p q : Point) : Prop := |
| 28 | p ≠ q ∧ ∀ r ∈ P, r ∉ openSegment ℝ p q |
| 29 | |
| 30 | /-- The point-visibility graph of `P`; its vertices retain their membership proofs. -/ |
| 31 | def visibilityGraph (P : Finset Point) : SimpleGraph P where |
| 32 | Adj p q := Visible P p q |
| 33 | symm := ⟨fun p q hpq ↦ |
| 34 | ⟨hpq.1.symm, fun r hr ↦ (openSegment_symm ℝ q.val p.val) ▸ hpq.2 r hr⟩⟩ |
| 35 | loopless := ⟨fun p hp => hp.1 rfl⟩ |
| 36 | |
| 37 | /-- The finite point set contains four distinct collinear points. -/ |
| 38 | def HasFourCollinear (P : Finset Point) : Prop := |
| 39 | ∃ f : Fin 4 → Point, |
| 40 | Function.Injective f ∧ (∀ i, f i ∈ P) ∧ Collinear ℝ (Set.range f) |
| 41 | |
| 42 | /-- The finite point set contains three distinct collinear points. -/ |
| 43 | def HasThreeCollinear (P : Finset Point) : Prop := |
| 44 | ∃ f : Fin 3 → Point, |
| 45 | Function.Injective f ∧ (∀ i, f i ∈ P) ∧ Collinear ℝ (Set.range f) |
| 46 | |
| 47 | /-- The finite point set contains `k` points that pairwise see one another. -/ |
| 48 | def HasVisibleClique (P : Finset Point) (k : ℕ) : Prop := |
| 49 | ∃ f : Fin k → Point, |
| 50 | Function.Injective f ∧ (∀ i, f i ∈ P) ∧ |
| 51 | Set.Pairwise (Set.range f) (Visible P) |
| 52 | |
| 53 | end Lax570090.Geometry |
| 54 |
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments