convex_iff_openSegment_subset — Mathlib

English

A set s is convex iff for any x,y ∈ s, the open segment between x and y is contained in s.

Русский

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

LaTeX

$$$\Convex 𝕜 s \iff \forall x \in s, \forall y \in s, openSegment 𝕜 x y \subseteq s$$$

Lean4

theorem convex_iff_openSegment_subset [ZeroLEOneClass 𝕜] :
    Convex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → openSegment 𝕜 x y ⊆ s :=
  forall₂_congr fun _ => starConvex_iff_openSegment_subset

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