eq_of_isVisible_of_left_mem — Mathlib

English

If s is open and x sees y through s, and y ∈ s, then x = y.

Русский

Если s открыто и x видит y через s, и y ∈ s, тогда x = y.

LaTeX

$$$\text{IsOpen } s\ \&\ \text{IsVisible } 𝕜\ s\ x\ y\ \&\ y\in s\ \Rightarrow\ x=y$$$

Lean4

/-- One cannot see any point of an open set. -/
theorem eq_of_isVisible_of_left_mem (hs : IsOpen s) (hsxy : IsVisible 𝕜 s x y) (hy : y ∈ s) : x = y :=
  hsxy.eq_of_mem_interior (by simpa [hs.interior_eq])

Похожие утверждения