isCompact

Mathlib.Analysis.Convex.Body

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

English

As above, isCompact holds for convex bodies treated as sets within V.

Русский

Как выше, для выпуклого тела выполнено свойство компактности рассматриваемого множества внутри V.

LaTeX

$$$IsCompact(K)$$$

Lean4

protected theorem isCompact (K : ConvexBody V) : IsCompact (K : Set V) :=
  K.isCompact'

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

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

Разделы

Аффилиация

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