absConvexHull_mono

Mathlib.Analysis.LocallyConvex.AbsConvex

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

English

If s ⊆ t then absConvexHull 𝕜 s ⊆ absConvexHull 𝕜 t.

Русский

Если s ⊆ t, то absConvexHull 𝕜 s ⊆ absConvexHull 𝕜 t.

LaTeX

$$$$ s \\subseteq t \\Rightarrow \\operatorname{absConvexHull}_{\\mathbb{k}}(s) \\subseteq \\operatorname{absConvexHull}_{\\mathbb{k}}(t). $$$$

Lean4

@[mono, gcongr]
theorem absConvexHull_mono (hst : s ⊆ t) : absConvexHull 𝕜 s ⊆ absConvexHull 𝕜 t :=
  (absConvexHull 𝕜).monotone hst

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

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

Разделы

Аффилиация

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