segment_subset — Mathlib

English

If s is star-convex at x, then for each y ∈ s, the segment from x to y lies in s.

Русский

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

LaTeX

$$$$StarConvex_{\mathbb{K}}(x,s) \implies \forall y \in s,\ [x -[\mathbb{K}] y] \subseteq s.$$$$

Lean4

theorem segment_subset (h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) : [x -[𝕜] y] ⊆ s :=
  starConvex_iff_segment_subset.1 h hy

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