starConvex_iff — Mathlib

English

If s is convex, then for any x, StarConvex 𝕜 x s is equivalent to x ∈ s provided s is nonempty.

Русский

Если s выпукло и непусто, тогда StarConvex 𝕜 x s эквивалентно x ∈ s.

LaTeX

$$$\text{StarConvex 𝕜 x s} \iff x \in s$ (assuming $s$ convex and nonempty)$$

Lean4

theorem starConvex_iff [ZeroLEOneClass 𝕜] (hs : Convex 𝕜 s) (h : s.Nonempty) : StarConvex 𝕜 x s ↔ x ∈ s :=
  ⟨fun hxs => hxs.mem h, hs.starConvex⟩

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