English
One cannot see a distinct point lying in the interior of a set: if x sees y with respect to s and y lies in the interior of s, then x must equal y.
Русский
Нельзя увидеть точку, лежащую внутри множества: если x видит y относительно s и y ∈ interior(s), то x = y.
LaTeX
$$$IsVisible\ 𝕜\ s\ x\ y \wedge y\in int(s) \Rightarrow x=y$$$
Lean4
/-- One cannot see any point in the interior of a set. -/
theorem eq_of_mem_interior (hsxy : IsVisible 𝕜 s x y) (hy : y ∈ interior s) : x = y :=
by
by_contra! hxy
suffices h : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False by obtain ⟨_, ⟨⟩⟩ := h.exists
have hmem : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, lineMap y x δ ∈ s :=
lineMap_continuous.continuousWithinAt.eventually_mem (by simpa using mem_interior_iff_mem_nhds.1 hy)
filter_upwards [hmem, Ioo_mem_nhdsGT zero_lt_one] with δ hmem hsbt using hsxy.symm hmem (by aesop)
