absConvexHull_univ

Mathlib.Analysis.LocallyConvex.AbsConvex

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

English

absConvexHull 𝕜 univ = univ.

Русский

absConvexHull 𝕜 единичного множества равна единичному.

LaTeX

$$$$ \\operatorname{absConvexHull}_{\\mathbb{k}}(\\mathrm{univ}) = \\mathrm{univ}. $$$$

Lean4

@[simp]
theorem absConvexHull_univ : absConvexHull 𝕜 (univ : Set E) = univ :=
  ClosureOperator.closure_top (absConvexHull 𝕜)

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

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

Разделы

Аффилиация

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