absConvexHull_eq_self

Mathlib.Analysis.LocallyConvex.AbsConvex

URI: https://scilib.ai/kg/mathlib#absConvexHull_eq_self

English

The hull equality absConvexHull 𝕜 s = s is equivalent to s being absolutely convex.

Русский

Замыкание по абс-конвексности эквивалентно тому, что s абсолютно выпукло.

LaTeX

$$$absConvexHull 𝕜 s = s \\iff AbsConvex 𝕜 s$$$

Lean4

theorem absConvexHull_eq_self : absConvexHull 𝕜 s = s ↔ AbsConvex 𝕜 s :=
  (absConvexHull 𝕜).isClosed_iff.symm

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

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

Разделы

Аффилиация

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