convex_iff_segment_subset — Mathlib

English

A set s is convex iff every segment between two points of s lies in s.

Русский

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

LaTeX

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

Lean4

theorem convex_iff_segment_subset : Convex 𝕜 s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s :=
  forall₂_congr fun _ _ => starConvex_iff_segment_subset

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