IsVisible — Mathlib

English

Visibility through a set is symmetric: x sees y through s iff y sees x through s.

Русский

Видимость через множество симметрична: если x видит y через s, то y видит x через s.

LaTeX

$$IsVisible 𝕜 s x y ⇔ IsVisible 𝕜 s y x$$

Lean4

/-- Two points are visible to each other through a set if no point of that set lies strictly
between them.

By convention, a point `x` sees itself through any set `s`, even when `x ∈ s`. -/
def IsVisible (s : Set P) (x y : P) : Prop :=
  ∀ ⦃z⦄, z ∈ s → ¬Sbtw 𝕜 x z y

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