Theorems · Theorem · convex and discrete geometry

IsVisible.mem_convexHull_isVisible

∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {x y : V},
  x ∉ (convexHull ℝ) s →
    y ∈ (convexHull ℝ) s →
      IsVisible ℝ ((convexHull ℝ) s) x y → y ∈ (convexHull ℝ) {z | 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.

Defined in

Mathlib.Analysis.Convex.Visible

Cited by

1 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupModule