English
Let s be a subset of a space P and let x,y ∈ P with x ≠ y. Then x sees y through s if and only if every interior point of the line segment from x to y lies outside s; equivalently, for every δ with 0 < δ < 1, the point lineMap x y δ is not in s.
Русский
Пусть s ⊆ P. Пусть x,y ∈ P и x ≠ y. Тогда x видит y через s тогда и только если каждая внутренняя точка отрезка между x и y лежит вне s; эквивалентно: для любого δ, 0 < δ < 1, точка lineMap x y δ не принадлежит s.
LaTeX
$$$\text{IsVisible }\ 𝕜\ s\ x\ y\quad\text{ iff }\quad x\neq y\ \Rightarrow\ \forall \delta\in(0,1):\ lineMap\ x\ y\ \delta\notin s$$$
Lean4
theorem isVisible_iff_lineMap (hxy : x ≠ y) : IsVisible 𝕜 s x y ↔ ∀ δ ∈ Set.Ioo (0 : 𝕜) 1, lineMap x y δ ∉ s :=
by
simp [IsVisible, sbtw_iff_mem_image_Ioo_and_ne, hxy]
aesop
