toStrictConvexSpace — Mathlib

English

Two points are visible to each other through a set if no point of that set lies strictly between them; a point sees itself through any set.

Русский

Две точки видны друг другу через множество, если ни одна точка этого множества не лежит строго между ними; точка видит себя через любое множество.

LaTeX

$$IsVisible 𝕜 s x y := ∀ z∈s, ¬Sbtw 𝕜 x z y$$

Lean4

instance (priority := 100) toStrictConvexSpace : StrictConvexSpace ℝ E :=
  StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy hxy =>
    let ⟨_, hδ, h⟩ := exists_forall_closed_ball_dist_add_le_two_sub E (norm_sub_pos_iff.2 hxy)
    ((h hx.le hy.le le_rfl).trans_lt <| sub_lt_self _ hδ).ne

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