sub

Mathlib.Analysis.Convex.Strict

URI: https://scilib.ai/kg/mathlib#StrictConvex.sub

English

If s is strictly convex, then the negation -s is strictly convex.

Русский

Если S строго выпукло, то множество −S также строго выпукло.

LaTeX

$$$\StrictConvex 𝕜 s \Rightarrow \StrictConvex 𝕜 (-s)$$$

Lean4

theorem sub (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s - t) :=
  (sub_eq_add_neg s t).symm ▸ hs.add ht.neg

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

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

Разделы

Аффилиация

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