openSegment_subset — Mathlib

English

If s is star-convex at x, then the open segment from x to any y ∈ s is contained in s.

Русский

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

LaTeX

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

Lean4

theorem openSegment_subset (h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s :=
  (openSegment_subset_segment 𝕜 x y).trans (h.segment_subset hy)

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