openSegment_subset — Mathlib

English

If s is convex, then the open segment between x and y is contained in s for x,y ∈ s.

Русский

Если s выпукло, то открытый отрезок между x и y содержится в s для x,y ∈ s.

LaTeX

$$$\forall x,y\in s,\ \text{openSegment}_{𝕜}(x,y) \subseteq s$$$

Lean4

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

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