smul_preimage

Mathlib.Analysis.Convex.Basic

URI: https://scilib.ai/kg/mathlib#Convex.smul_preimage

English

If s is convex, then its preimage under scalar multiplication by c is convex.

Русский

Если множество выпукло, то его предобраз под умножением на скаляр c выпукл.

LaTeX

$$$$ \\operatorname{Convex}_{\\mathbb{K}}\\bigl( (\\cdot c)^{-1}(s) \\bigr) $$$$

Lean4

theorem smul_preimage (hs : Convex 𝕜 s) (c : 𝕜) : Convex 𝕜 ((fun z => c • z) ⁻¹' s) :=
  hs.linear_preimage (LinearMap.lsmul _ _ c)

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

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

Разделы

Аффилиация

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