Points in sight

This file defines the relation of visibility with respect to a set, and lower bounds how many elements of a set a point sees in terms of the dimension of that set.

TODO

The art gallery problem can be stated using the visibility predicate: A set A (the art gallery) is guarded by a finite set G (the guards) iff ∀ a ∈ A, ∃ g ∈ G, IsVisible ℝ sᶜ a g.

def IsVisible (𝕜 : Type u_1) {V : Type u_2} {P : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] (s : Set P) (x y : P) : Prop

Two points are visible to each other through a set if no point of that set lies strictly between them.

By convention, a point x sees itself through any set s, even when x ∈ s.

Equations

• IsVisible 𝕜 s x y = ∀ ⦃z : P⦄, z ∈ s → ¬Sbtw 𝕜 x z y

@[simp]

theorem IsVisible.rfl {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] {s : Set P} {x : P} : IsVisible 𝕜 s x x

theorem isVisible_comm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] {s : Set P} {x y : P} : IsVisible 𝕜 s x y ↔ IsVisible 𝕜 s y x

theorem IsVisible.symm {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] {s : Set P} {x y : P} : IsVisible 𝕜 s x y → IsVisible 𝕜 s y x

Alias of the forward direction of isVisible_comm.

theorem IsVisible.mono {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] {s t : Set P} {x y : P} (hst : s ⊆ t) (ht : IsVisible 𝕜 t x y) : IsVisible 𝕜 s x y

theorem isVisible_iff_lineMap {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] [AddTorsor V P] {s : Set P} {x y : P} (hxy : x ≠ y) : IsVisible 𝕜 s x y ↔ ∀ δ ∈ Set.Ioo 0 1, (AffineMap.lineMap x y) δ ∉ s

theorem IsVisible.of_convexHull_of_pos {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {s : Set V} {x : V} {ι : Type u_4} {t : Finset ι} {a : ι → V} {w : ι → 𝕜} (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i ∈ t, w i = 1) (ha : ∀ i ∈ t, a i ∈ s) (hx : x ∉ (convexHull 𝕜) s) (hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)) {i : ι} (hi : i ∈ t) (hwi : 0 < w i) : IsVisible 𝕜 ((convexHull 𝕜) s) x (a i)

If a point x sees a convex combination of points of a set s through convexHull ℝ s ∌ x, then it sees all terms of that combination.

Note that the converse does not hold.

theorem IsVisible.eq_of_mem_interior {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {s : Set V} {x y : V} [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] (hsxy : IsVisible 𝕜 s x y) (hy : y ∈ interior s) : x = y

One cannot see any point in the interior of a set.

theorem IsOpen.eq_of_isVisible_of_left_mem {𝕜 : Type u_1} {V : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup V] [Module 𝕜 V] {s : Set V} {x y : V} [TopologicalSpace 𝕜] [OrderTopology 𝕜] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] (hs : IsOpen s) (hsxy : IsVisible 𝕜 s x y) (hy : y ∈ s) : x = y

One cannot see any point of an open set.

theorem IsVisible.mem_convexHull_isVisible {V : Type u_2} [AddCommGroup V] [Module ℝ V] {s : Set V} {x y : V} (hx : x ∉ (convexHull ℝ) s) (hy : y ∈ (convexHull ℝ) s) (hxy : IsVisible ℝ ((convexHull ℝ) s) x y) : y ∈ (convexHull ℝ) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

All points of the convex hull of a set s visible from a point x ∉ convexHull ℝ s lie in the convex hull of such points that actually lie in s.

Note that the converse does not hold.

theorem IsClosed.exists_wbtw_isVisible {V : Type u_2} [AddCommGroup V] [Module ℝ V] {s : Set V} {y : V} [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] (hs : IsClosed s) (hy : y ∈ s) (x : V) : ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

If s is a closed set, then any point x sees some point of s in any direction where there is something to see.

theorem IsClosed.convexHull_subset_affineSpan_isVisible {V : Type u_2} [AddCommGroup V] [Module ℝ V] {s : Set V} {x : V} [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] (hs : IsClosed ((convexHull ℝ) s)) (hx : x ∉ (convexHull ℝ) s) : (convexHull ℝ) s ⊆ ↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}))

A set whose convex hull is closed lies in the cone based at a point x generated by its points visible from x through its convex hull.

theorem rank_le_card_isVisible {V : Type u_2} [AddCommGroup V] [Module ℝ V] {s : Set V} {x : V} [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul ℝ V] (hs : IsClosed ((convexHull ℝ) s)) (hx : x ∉ (convexHull ℝ) s) : Module.rank ℝ ↥(Submodule.span ℝ (-x +ᵥ s)) ≤ Cardinal.mk ↑{y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x y}

If s is a closed set of dimension d and x is a point outside of its convex hull, then x sees at least d points of the convex hull of s that actually lie in s.