convexHull_mono

Mathlib.Analysis.Convex.Hull

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

English

If s is contained in t, then the convex hull of s is contained in the convex hull of t.

Русский

Если s ⊆ t, то выпуклая оболочка s ⊆ выпуклая оболочка t.

LaTeX

$$$ (hst : s \\subseteq t) : convexHull 𝕜 s \\subseteq convexHull 𝕜 t $$$

Lean4

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

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

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

Разделы

Аффилиация

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