English
If s is closed and y ∈ s, then for any x there exists z ∈ s such that Wbtw x z y and z is visible from x through s.
Русский
Если s замкнуто, и y ∈ s, то при любом x существует z ∈ s такой, что Wbtw x z y и z видно из x через s.
LaTeX
$$$\text{IsClosed } s \Rightarrow \forall y\in s\, \forall x\, \exists z\in s,\ (Wbtw\mathbb{R}\ x\ z\ y)\ \land\ IsVisible\ 𝕜\ s\ x\ z$$$
Lean4
/-- 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 exists_wbtw_isVisible (hs : IsClosed s) (hy : y ∈ s) (x : V) : ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z :=
by
let t : Set ℝ := Ici 0 ∩ lineMap x y ⁻¹' s
have ht₁ : 1 ∈ t := by simpa [t]
have ht : BddBelow t := bddBelow_Ici.inter_of_left
let δ : ℝ := sInf t
have hδ₁ : δ ≤ 1 := csInf_le ht ht₁
obtain ⟨hδ₀, hδ⟩ : 0 ≤ δ ∧ lineMap x y δ ∈ s :=
(isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht
refine ⟨lineMap x y δ, hδ, wbtw_lineMap_iff.2 <| .inr ⟨hδ₀, hδ₁⟩, ?_⟩
rintro _ hε ⟨⟨ε, ⟨hε₀, hε₁⟩, rfl⟩, -, h⟩
replace hδ₀ : 0 < δ := hδ₀.lt_of_ne' <| by rintro hδ₀; simp [hδ₀] at h
replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp at h
rw [lineMap_lineMap_right] at hε
exact (csInf_le ht ⟨mul_nonneg hε₀ hδ₀.le, hε⟩).not_gt <| mul_lt_of_lt_one_left hδ₀ hε₁
