English
If the convex hull of s is closed and x ∉ convexHull 𝕜 s, then the rank of span of (−x + s) is bounded above by the cardinality of the set of visible points from x in s.
Русский
Если выпуклая оболочка s замкнута и x ∉ conv(s), то ранг пространства, породимого −x + s, не превосходит кардинала множества точек s, видимых из x.
LaTeX
$$Module.rank ℝ (span ℝ (−x +ᵥ s)) ≤ #({y ∈ s | IsVisible 𝕜 (convexHull 𝕜 s) x y})$$
Lean4
/-- 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`. -/
theorem rank_le_card_isVisible (hs : IsClosed (convexHull ℝ s)) (hx : x ∉ convexHull ℝ s) :
Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤ #({y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) := by
calc
Module.rank ℝ (span ℝ (-x +ᵥ s)) ≤
Module.rank ℝ (span ℝ (-x +ᵥ affineSpan ℝ ({ x } ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V)) :=
by
push_cast
refine Submodule.rank_mono ?_
gcongr
exact (subset_convexHull ..).trans <| hs.convexHull_subset_affineSpan_isVisible hx
_ = Module.rank ℝ (span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y})) :=
by
suffices h :
-x +ᵥ (affineSpan ℝ ({ x } ∪ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) : Set V) =
span ℝ (-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y})
by rw [AffineSubspace.coe_pointwise_vadd, h, span_span]
simp [← AffineSubspace.coe_pointwise_vadd, AffineSubspace.pointwise_vadd_span, vadd_set_insert, -coe_affineSpan,
affineSpan_insert_zero]
_ ≤ #(-x +ᵥ {y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) := (rank_span_le _)
_ = #({y ∈ s | IsVisible ℝ (convexHull ℝ s) x y}) := by simp
