Theorems · Theorem · convex and discrete geometry

rank_le_card_isVisible

∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {x : V} [inst_2 : TopologicalSpace V]
  [IsTopologicalAddGroup V] [ContinuousSMul ℝ V],
  IsClosed ((convexHull ℝ) s) →
    x ∉ (convexHull ℝ) s →
      Module.rank ℝ ↥(Submodule.span ℝ (-x +ᵥ s)) ≤ Cardinal.mk ↑{y | 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.

Defined in

Mathlib.Analysis.Convex.Visible

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul