starConvex — Mathlib

English

A linear subspace is star-shaped with respect to the origin; in particular it is starConvex with center 0.

Русский

Линейное подпространство является звездообразной формой относительно начала координат; следовательно, оно starConvex с центром в 0.

LaTeX

$$$\text{StarConvex}_{\mathbb{K}}(0, K).$$$

Lean4

protected theorem starConvex (K : Submodule 𝕜 E) : StarConvex 𝕜 (0 : E) K :=
  K.convex K.zero_mem

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