convex — Mathlib

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

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