mem — Mathlib

English

If s is star-convex at x and s is nonempty, then x ∈ s (assuming 0 ≤ 1 in the scalar class).

Русский

Если s звездообразно относительно x и не пусто, то x ∈ s (при условии, что 0 ≤ 1 в классе скаляров).

LaTeX

$$$$StarConvex_{\mathbb{K}}(x,s) \land s \neq \varnothing \Rightarrow x \in s.$$$$

Lean4

theorem mem [ZeroLEOneClass 𝕜] (hs : StarConvex 𝕜 x s) (h : s.Nonempty) : x ∈ s :=
  by
  obtain ⟨y, hy⟩ := h
  convert hs hy zero_le_one le_rfl (add_zero 1)
  rw [one_smul, zero_smul, add_zero]

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