smul_mem

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ConvexCone.smul_mem

English

If c > 0 and x ∈ C, then c • x ∈ C.

Русский

Если c > 0 и x ∈ C, то c • x ∈ C.

LaTeX

$$$c > 0 \\land x \\in C \\Rightarrow c \\cdot x \\in C$$$

Lean4

@[aesop 90% (rule_sets := [SetLike])]
protected theorem smul_mem (hc : 0 < c) (hx : x ∈ C) : c • x ∈ C :=
  C.smul_mem' hc hx

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru