definition
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
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.
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 Lax56.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 := by |
| 34 | intro p q hpq |
| 35 | refine ⟨hpq.1.symm, ?_⟩ |
| 36 | simpa only [openSegment_symm] using hpq.2 |
| 37 | loopless := ⟨fun p hp => hp.1 rfl⟩ |
| 38 | |
| 39 | /-- The finite point set contains four distinct collinear points. -/ |
| 40 | def HasFourCollinear (P : Finset Point) : Prop := |
| 41 | ∃ f : Fin 4 → Point, |
| 42 | Function.Injective f ∧ (∀ i, f i ∈ P) ∧ Collinear ℝ (Set.range f) |
| 43 | |
| 44 | /-- The finite point set contains three distinct collinear points. -/ |
| 45 | def HasThreeCollinear (P : Finset Point) : Prop := |
| 46 | ∃ f : Fin 3 → Point, |
| 47 | Function.Injective f ∧ (∀ i, f i ∈ P) ∧ Collinear ℝ (Set.range f) |
| 48 | |
| 49 | /-- The finite point set contains `k` points that pairwise see one another. -/ |
| 50 | def HasVisibleClique (P : Finset Point) (k : ℕ) : Prop := |
| 51 | ∃ f : Fin k → Point, |
| 52 | Function.Injective f ∧ (∀ i, f i ∈ P) ∧ |
| 53 | Set.Pairwise (Set.range f) (Visible P) |
| 54 | |
| 55 | end Lax56.Geometry |
| 56 |
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments