segment_subset

Mathlib.Analysis.Convex.Basic

URI: https://scilib.ai/kg/mathlib#Convex.segment_subset

English

If s is convex, then for any x,y ∈ s, the segment [x,y] is contained in s.

Русский

Если s выпукло, то для любых x,y ∈ s отрезок [x,y] содержится в s.

LaTeX

$$$\forall x,y\in s,\ [x-\!\!_{𝕜}y] \subseteq s$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru