Theorems · Theorem · convex and discrete geometry

IsClosed.exists_wbtw_isVisible

∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {y : V} [inst_2 : TopologicalSpace V]
  [IsTopologicalAddGroup V] [ContinuousSMul ℝ V],
  IsClosed s → 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.

Defined in

Mathlib.Analysis.Convex.Visible

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul