starConvex_iff_segment_subset — Mathlib

English

A set s is star-convex with respect to x if and only if for every y ∈ s the segment from x to y is contained in s.

Русский

Множество s звездообразно относительно точки x тогда и только тогда, когда для каждого y ∈ s отрезок от x до y содержится в s.

LaTeX

$$$$StarConvex_{\mathbb{K}}(x,s) \iff \forall y \in s,\ [x -[\mathbb{K}] y] \subseteq s.$$$$

Lean4

theorem starConvex_iff_segment_subset : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s :=
  by
  constructor
  · rintro h y hy z ⟨a, b, ha, hb, hab, rfl⟩
    exact h hy ha hb hab
  · rintro h y hy a b ha hb hab
    exact h hy ⟨a, b, ha, hb, hab, rfl⟩

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