starConvex — Mathlib

English

If s is balanced, then it is star-convex with respect to the origin: for every y ∈ s and t ∈ [0,1], t y ∈ s.

Русский

Если s сбалансировано, то оно звездо-выпукло относительно нуля: для любого y ∈ s и t ∈ [0,1] верно t y ∈ s.

LaTeX

$$$$\\text{If } s \\text{ is balanced, then } \\operatorname{StarConvex}_{\\mathbb{R}}(0,S).$$$$

Lean4

theorem starConvex (hs : Balanced ℝ s) : StarConvex ℝ 0 s :=
  starConvex_zero_iff.2 fun _ hx a ha₀ ha₁ => hs _ (by rwa [Real.norm_of_nonneg ha₀]) (smul_mem_smul_set hx)

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