instAdd

Mathlib.Analysis.Convex.Body

URI: https://scilib.ai/kg/mathlib#ConvexBody.instAdd

English

Convexity property for ConvexBody extends to related constructions.

Русский

Свойство выпуклости сохраняется в сопутствующих конструкциях ConvexBody.

LaTeX

$$$K.convex$$$

Lean4

instance : Add (ConvexBody V) where
  add K L := ⟨K + L, K.convex.add L.convex, K.isCompact.add L.isCompact, K.nonempty.add L.nonempty⟩

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

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

Разделы

Аффилиация

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