starConvex_iff_openSegment_subset

English

If x ∈ s and star-convex, then openSegment from x to any y ∈ s is contained in s; conversely, containment for all such y characterizes star-convexity.

Русский

Если x ∈ s и s звездообразно, то открытый сегмент от x до любого y ∈ s содержится в s; наоборот, вложение открытых сегментов по всем y характеризует звездообразность.

LaTeX

$$$$StarConvex_{\mathbb{K}}(x,s) \iff \forall y\in s,\ openSegment_{\mathbb{K}}(x,y) \subseteq s.$$$$

Lean4

theorem starConvex_iff_openSegment_subset [ZeroLEOneClass 𝕜] (hx : x ∈ s) :
    StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → openSegment 𝕜 x y ⊆ s :=
  starConvex_iff_segment_subset.trans <| forall₂_congr fun _ hy => (openSegment_subset_iff_segment_subset hx hy).symm

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