English
If K is a submodule of a vector space E over 𝕜, then K, viewed as a subset of E, is convex.
Русский
Если K — подмодуль векторного пространства E над 𝕜, то множество K (рассматриваемое как подмножество E) выпукло.
LaTeX
$$$K \subseteq E$ суть: \operatorname{Convex}_{\mathbb{K}}(K).$$$
Lean4
protected theorem convex (K : Submodule 𝕜 E) : Convex 𝕜 (↑K : Set E) :=
by
repeat' intro
refine add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_) <;> assumption